/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.parse.visitor;

import java.io.ByteArrayOutputStream;
import java.io.File;
import java.io.FileNotFoundException;
import java.io.FileReader;
import java.io.PrintStream;
import java.io.Reader;
import java.io.StringReader;
import java.util.ArrayList;
import java.util.Collections;
import java.util.Enumeration;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.Vector;

import javax.help.Map.ID;

import alloy.ast.ArgList;
import alloy.ast.ArrowMultExpr;
import alloy.ast.Assertion;
import alloy.ast.Assertions;
import alloy.ast.BinaryExpr;
import alloy.ast.BinaryExprOp;
import alloy.ast.BinaryFormula;
import alloy.ast.BinaryIntExpr;
import alloy.ast.CardinalityExpr;
import alloy.ast.CheckCommand;
import alloy.ast.Commands;
import alloy.ast.CompOp;
import alloy.ast.ComprehensionExpr;
import alloy.ast.Decl;
import alloy.ast.Decls;
import alloy.ast.DummyNode;
import alloy.ast.ElemFormula;
import alloy.ast.ElemIntFormula;
import alloy.ast.EmptyExpr;
import alloy.ast.EmptyFormula;
import alloy.ast.EmptySetExpr;
import alloy.ast.Expr;
import alloy.ast.ExprCastIntExpr;
import alloy.ast.Exprs;
import alloy.ast.Fact;
import alloy.ast.Facts;
import alloy.ast.Formula;
import alloy.ast.FormulaSeq;
import alloy.ast.Formulas;
import alloy.ast.Function;
import alloy.ast.Functions;
import alloy.ast.GeneralScope;
import alloy.ast.Id;
import alloy.ast.IdentityExpr;
import alloy.ast.Ids;
import alloy.ast.IfThenElseExpr;
import alloy.ast.IfThenElseIntExpr;
import alloy.ast.ImplicationFormula;
import alloy.ast.IntCompOp;
import alloy.ast.IntExpr;
import alloy.ast.IntExprCastExpr;
import alloy.ast.IntExprOp;
import alloy.ast.IntNode;
import alloy.ast.InvocationExpr;
import alloy.ast.InvocationFormula;
import alloy.ast.LetDecl;
import alloy.ast.LetDecls;
import alloy.ast.LetExpr;
import alloy.ast.LetFormula;
import alloy.ast.LetIntExpr;
import alloy.ast.LiteralIntExpr;
import alloy.ast.Location;
import alloy.ast.LogicOp;
import alloy.ast.Module;
import alloy.ast.ModuleId;
import alloy.ast.Modules;
import alloy.ast.Multiplicity;
import alloy.ast.MultiplicityExpr;
import alloy.ast.MultiplicityFormula;
import alloy.ast.NegFormula;
import alloy.ast.Path;
import alloy.ast.Predicate;
import alloy.ast.Predicates;
import alloy.ast.QualifiedName;
import alloy.ast.QualifiedNames;
import alloy.ast.Qualifier;
import alloy.ast.Qualifiers;
import alloy.ast.QuantifiedExpr;
import alloy.ast.QuantifiedFormula;
import alloy.ast.Quantifier;
import alloy.ast.RunCommand;
import alloy.ast.Scope;
import alloy.ast.SetMultExpr;
import alloy.ast.SigExpr;
import alloy.ast.SigExprs;
import alloy.ast.Signature;
import alloy.ast.Signatures;
import alloy.ast.SpecificScope;
import alloy.ast.Specification;
import alloy.ast.SumExpr;
import alloy.ast.SumIntExpr;
import alloy.ast.TreeNode;
import alloy.ast.TypeScope;
import alloy.ast.TypeScopes;
import alloy.ast.UnaryExpr;
import alloy.ast.UnaryExprOp;
import alloy.ast.UniversalExpr;
import alloy.ast.Variable;
import alloy.ast.VariableExpr;
import alloy.ast.Variables;
import alloy.parse.AlloyParser;
import alloy.parse.AlloyPrepass;
import alloy.parse.Environment;
import alloy.parse.ParseException;
import alloy.parse.Token;
import alloy.parse.TokenMgrError;
import alloy.parse.syntaxtree.AliasCST;
import alloy.parse.syntaxtree.AndFormulaCST;
import alloy.parse.syntaxtree.AndOpCST;
import alloy.parse.syntaxtree.AssertionCST;
import alloy.parse.syntaxtree.BinaryIntExprCST;
import alloy.parse.syntaxtree.BracketOrDotExprCST;
import alloy.parse.syntaxtree.CheckCST;
import alloy.parse.syntaxtree.CompOpCST;
import alloy.parse.syntaxtree.DeclCST;
import alloy.parse.syntaxtree.DirCST;
import alloy.parse.syntaxtree.DomainExprCST;
import alloy.parse.syntaxtree.EquivOpCST;
import alloy.parse.syntaxtree.EquivalenceFormulaCST;
import alloy.parse.syntaxtree.ExprCST;
import alloy.parse.syntaxtree.ExtensionCST;
import alloy.parse.syntaxtree.FactCST;
import alloy.parse.syntaxtree.FormulaBodyCST;
import alloy.parse.syntaxtree.FormulaCST;
import alloy.parse.syntaxtree.FormulaSeqCST;
import alloy.parse.syntaxtree.FunctionCST;
import alloy.parse.syntaxtree.ImplicationFormulaCST;
import alloy.parse.syntaxtree.ImportCST;
import alloy.parse.syntaxtree.IntCompOpCST;
import alloy.parse.syntaxtree.IntExprCST;
import alloy.parse.syntaxtree.IntOpCST;
import alloy.parse.syntaxtree.IntersectExprCST;
import alloy.parse.syntaxtree.InvocationBaseCST;
import alloy.parse.syntaxtree.InvocationExprCST;
import alloy.parse.syntaxtree.LetDeclCST;
import alloy.parse.syntaxtree.LetExprCST;
import alloy.parse.syntaxtree.ModuleCST;
import alloy.parse.syntaxtree.ModuleDeclCST;
import alloy.parse.syntaxtree.ModuleNameCST;
import alloy.parse.syntaxtree.ModulePathCST;
import alloy.parse.syntaxtree.MultCST;
import alloy.parse.syntaxtree.MultExprCST;
import alloy.parse.syntaxtree.NegOpCST;
import alloy.parse.syntaxtree.Node;
import alloy.parse.syntaxtree.NodeChoice;
import alloy.parse.syntaxtree.NodeList;
import alloy.parse.syntaxtree.NodeListOptional;
import alloy.parse.syntaxtree.NodeOptional;
import alloy.parse.syntaxtree.NodeSequence;
import alloy.parse.syntaxtree.NodeToken;
import alloy.parse.syntaxtree.OrFormulaCST;
import alloy.parse.syntaxtree.OrOpCST;
import alloy.parse.syntaxtree.OtherExprCST;
import alloy.parse.syntaxtree.OtherFormulaCST;
import alloy.parse.syntaxtree.OtherIntExprCST;
import alloy.parse.syntaxtree.PackageNameCST;
import alloy.parse.syntaxtree.ParaNameCST;
import alloy.parse.syntaxtree.ParagraphCST;
import alloy.parse.syntaxtree.PredicateCST;
import alloy.parse.syntaxtree.QualifierCST;
import alloy.parse.syntaxtree.QuantOrLetFormulaCST;
import alloy.parse.syntaxtree.QuantifierCST;
import alloy.parse.syntaxtree.RangeExprCST;
import alloy.parse.syntaxtree.RelMultExprCST;
import alloy.parse.syntaxtree.RelationExprCST;
import alloy.parse.syntaxtree.RelationalOverrideExprCST;
import alloy.parse.syntaxtree.RunCST;
import alloy.parse.syntaxtree.ScopeCST;
import alloy.parse.syntaxtree.SigCST;
import alloy.parse.syntaxtree.SigNameCST;
import alloy.parse.syntaxtree.SigQualCST;
import alloy.parse.syntaxtree.SignatureCST;
import alloy.parse.syntaxtree.SpecificationCST;
import alloy.parse.syntaxtree.SumOrLetIntExprCST;
import alloy.parse.syntaxtree.TypeArgCST;
import alloy.parse.syntaxtree.TypeArgsCST;
import alloy.parse.syntaxtree.TypeParameterCST;
import alloy.parse.syntaxtree.TypeParametersCST;
import alloy.parse.syntaxtree.TypeScopeCST;
import alloy.parse.syntaxtree.TypeVarCST;
import alloy.parse.syntaxtree.TypeVarsCST;
import alloy.parse.syntaxtree.UnOpCST;
import alloy.parse.syntaxtree.UnionDiffExprCST;
import alloy.parse.syntaxtree.UnionDiffOpCST;
import alloy.parse.syntaxtree.UnopExprCST;
import alloy.parse.syntaxtree.VarCST;
import alloy.util.Dbg;
import alloy.util.FileUtil;
import alloy.util.Msg;

/**
 * <p>A concrete syntax tree visitor which constructs the corresponding
 * abstract syntax tree.  This visitor encapsulates the complexities (ugliness)
 * of the concrete syntax tree generated by JTB, so that after the visitor
 * is run, only our cleaner AST is used.  To understand this visitor, first
 * read the JTB documentation.
 * @see <a href="http://www.cs.purdue.edu/jtb/docs.html">JTB Documentation</a>
 */

final public class MakeASTVisitor extends ObjectDepthFirst {

    /** maps parse production names to more readable name */
    private final static Map _productionToName;

    // initialize the mapping
    static {
        final Map p = new HashMap();
        p.put("SpecificationCST", "the specification");
        p.put("ModuleCST", "a module");
        p.put("ModuleDeclCST", "a module declaration");
        p.put("ModuleNameCST", "a module name");
        p.put("PackageNameCST", "a qualified name");
        p.put("DirCST", "a qualified name");
        p.put("ImportCST", "an import statement");
        p.put("ModulePathCST", "a file path");
        p.put("ParagraphCST", "a paragraph");
        p.put("SignatureCST", "a signature");
        p.put("ExtensionCST", "an extends clause");
        p.put("FactCST", "a fact");
        p.put("AssertionCST", "an assertion");
        p.put("PredicateCST", "a predicate");
        p.put("FunctionCST", "a function");
        p.put("RunCST", "a run command");
        p.put("CheckCST", "a check command");
	p.put("ScopeCST", "a scope declaration");
        p.put("TypeScopeCST", "a scope declaration");
        p.put("DeclCST", "a declaration");
        p.put("QualifierCST", "a qualifier");
        p.put("MultExprCST", "a multiplicity expression");
        p.put("LetDeclCST", "a let declaration");
        p.put("ExprCST", "an expression");
        p.put("WithOrLetExprCST", "an expression");
        p.put("UnionDiffExprCST", "an expression");
        p.put("UnionDiffOpCST", "an expression");
        p.put("RelationalOverideExprCST", "an expression");
        p.put("IntersectExprCST", "an expression");
        p.put("RelationExprCST", "an expression");
        p.put("InvocationCST", "an invocation");
        p.put("BracketExprCST", "an expression");
        p.put("DotExprCST", "an expression");
        p.put("UnopExprCST", "an expression");
        p.put("DoubleColonExprCST", "an expression");
        p.put("OtherExprCST", "an expression");
        p.put("InvocationBaseCST", "an invocation");
        p.put("IntExprCST", "an int expression");
        p.put("SumWithOrLetIntExprCST", "an int expression");
        p.put("BinaryIntExprCST", "an int expression");
        p.put("OtherIntExprCST", "an int expression");
        p.put("IntOpCST", "an int expression");
        p.put("FormulaBodyCST", "a formula");
        p.put("FormulaSeqCST", "a formula");
        p.put("FormulaCST", "a formula");
        p.put("QuantWithOrLetFormulaCST", "a formula");
        p.put("OrFormulaCST", "a formula");
        p.put("OrOpCST", "a formula");
        p.put("EquivalenceFormulaCST", "a formula");
        p.put("EquivOpCST", "a formula");
        p.put("ImplicationFormulaCST", "a formula");
        p.put("ImpliesOpCST", "a formula");
        p.put("ElseOpCST", "a formula");
        p.put("AndFormulaCST", "a formula");
        p.put("AndOpCST", "a formula");
        p.put("OtherFormulaCST", "a formula");
        p.put("NegOpCST", "a formula");
        p.put("UnOpCST", "an expression");
        p.put("MultCST", "a multiplicity");
        p.put("CompOpCST", "a formula");
        p.put("IntCompOpCST", "an int expression");
        p.put("SigNameCST", "a signature name");
        p.put("SigCST", "a signature name");
        p.put("ParaNameCST", "a paragraph name");
        p.put("VarCST", "an identifier");
        p.put("QuantifierCST", "a quantifier");
        _productionToName = Collections.unmodifiableMap(p);
    }

    private static final String INT = "Int";
    private static final String UNIV = "univ";

	/** turns debug on/off */
	private boolean _debugSwitch;

    /** If no scope is specified for a given command, its default scope is set
     * to the value below.  This value is also the default scope of the built-in
     * Signature Int. **/
    private static final int DEFAULT_SCOPE = 3;

    /**
     * holds current module name, needed for all names
     * in each module
     */
    private QualifiedName _currentModuleName;

    /**
     * holds the path to the current module
     */
    private Path _curPath = new Path();

    /**
     * filename corresponding to CST
     */
    private final String _fileName;

    /**
     * holds the polymorphic type variables of current module
     */
    private Ids _polyTypeVarIds;

    /**
     * holds the a list of Ids (polymorphic type args) of all import statements
     * used to check whether imported more than once?
     */
    //private List _polyTypeArgIdsList; // List[Ids]

    /**
     * holds all the modules parsed so far.  only used to ensure
     * that a module does not get parsed twice.
     */
    private List _parsedModules;
    
    /**
     * holds all the modules parsed so far in depth first search. used to
     * prevent cycles.
     */
    private Set _importCycles;

    /**
     * holds the environment with all the bindings from typeVars to typeArgs
     */
    private Environment _environ;

    /**
     * holds a mapping of aliases to actual moduleNames
     */
    private Map _aliasesToModuleNames;  //QualifiedName -> QualifiedName

    /**
     * holds all the signature names
     */
    private Set _signatureNames;

    /** the modules in the alloy/lang package **/
    private Modules _lang;

    /** names of alloy/lang modules imported by the current module **/
    private QualifiedNames _importedLangModules;

    private MakeASTVisitor(String fileName_, Specification context_) {
	this(fileName_, new ArrayList(), new HashSet(), new Environment(true), context_.getLang()); 
    }

    private MakeASTVisitor(String fileName_, List parsedModules_, Set importCycles_, Environment environ_, 
			   Modules lang_) {
	_fileName = fileName_;
        _parsedModules = parsedModules_;
	_importCycles = importCycles_;
        _environ = environ_;
        _polyTypeVarIds = new Ids();
        _aliasesToModuleNames = new HashMap();
	_lang = lang_;
	_importedLangModules = new QualifiedNames();
	// alloy/lang/univ is opened by default
	_importedLangModules.addQualifiedName(_getLangModuleName(UNIV));
	// sanity checks for lang_ . . .
	Dbg.chk(lang_.numChildren() <= 2);
	Dbg.chk(((Module)lang_.childAt(0)).getName().equals(_getLangModuleName(UNIV)));
	Dbg.chk(lang_.numChildren()==1 || ((Module)lang_.childAt(1)).getName().equals(_getLangModuleName(INT)));
    }
    
    /** 
     * @return Modules containing the alloy/lang/Univ module.  The 
     * return Modules object does not contain the alloy/lang/Int module
     * since it is lazily imported
     **/
    private static Modules _getLang() {
	Modules lang = new Modules();
	lang.addModule(_getUnivModule());
	return lang;
    }

    /** @return constructs and returns the alloy/lang/univ module **/
    private static Module _getUnivModule() {
		
	// sig univ is abstract
	Signature univ = 
	    new Signature(Location.UNKNOWN, _getUnivName(),
			  new SigExprs(), new SigExprs(), new Decls(),
			  new Fact(new QualifiedName(new Id(UNIV + "Fact"), 
						     _getLangModuleName(UNIV))),
			  Multiplicity.SET,
			  false, true);
	
	Signatures sigs = new Signatures();
	sigs.addSignature(univ);
	
        return  new Module(_getLangModuleName(UNIV), sigs, new Facts(), new Predicates(), 
			   new Functions(), new Assertions(),
			   new Commands(), new QualifiedNames(), 
			   new QualifiedNames(), new QualifiedNames());

    }
    
    /**
     * given an alloy/lang/univ module, constructs an alloy/lang/Int module.
     **/
    private static Module _getIntModule(Module univModule_) {
	
	// Sig Int extends univ, just like all other sigs
	SigExprs intExtends = new SigExprs();
	intExtends.addSigExpr(((Signature) univModule_.getSignatures().
			       getSignatureIter().next()).toSigExpr());
	Signature Int = 
	    new Signature(Location.UNKNOWN, _getIntName(),
			  intExtends, new SigExprs(), new Decls(),	  
			  new Fact(new QualifiedName(new Id(INT+"Fact"), 
						     _getLangModuleName(INT))),
			  Multiplicity.SET,
			  false, false);

	Signatures sigs = new Signatures();
	sigs.addSignature(Int);

	// Int module opens univ module
	QualifiedNames openedModules = new QualifiedNames();
	openedModules.addQualifiedName((QualifiedName) univModule_.getName().copy());
	
	// Fact:  each Int represents a unique integer
	// all disj i, j : Int | int i != int j
	
	// disj i, j : Int
	Qualifiers quals = new Qualifiers();
	quals.addQualifier(Qualifier.DISJ);
	Variable i = new Variable(Id.generateId("i"));
	Variable j = new Variable(Id.generateId("j"));
	Variables vars = new Variables();
	vars.addVariable(i);
	vars.addVariable(j);
	SetMultExpr multExpr = new SetMultExpr(Multiplicity.NONE, Int.toSigExpr());
	Decls decls = new Decls();
	decls.addDecl(new Decl(quals,vars,multExpr));
	
	// int i
	ExprCastIntExpr iexpr = new ExprCastIntExpr(new VariableExpr((Variable)i.copy()));
	// int j
	ExprCastIntExpr jexpr = new ExprCastIntExpr(new VariableExpr((Variable)j.copy()));
	// int i != int j
	ElemIntFormula ineq = new ElemIntFormula(iexpr, 
	        IntCompOp.INT_NOTEQUALS, jexpr);
	
	//	 all disj i, j : Int | int i != int j
	Formula uniqueness = new QuantifiedFormula(Quantifier.ALL, 
	        decls, ineq, false); 
	
	Fact uniquenessFact = new Fact(new QualifiedName(new Id("IntsAreUnique"), 
		     				_getLangModuleName(INT)), new FormulaSeq(uniqueness));
	Facts facts = new Facts();
	facts.addFact(uniquenessFact);
	
	return  new Module(_getLangModuleName(INT), sigs, facts, new Predicates(), 
	        new Functions(), new Assertions(),
			   new Commands(), new QualifiedNames(), openedModules, 
			   new QualifiedNames());
    }

    /** @return Path to alloy/lang package **/
    private static Path _getLangPackagePath() {
	Ids packages = new Ids();
	packages.addId(new Id("alloy"));
	packages.addId(new Id("lang"));
	return new Path(packages);

    }
	
    /** @return QualifiedName for a non-polymorphic alloy/lang module with the given name. **/
    private static QualifiedName _getLangModuleName(String name) {
	return new QualifiedName(new ModuleId(name, new QualifiedNames()),
				 _getLangPackagePath());
    }

    /**@return fully qualified name of Signature univ  **/
    private static QualifiedName _getUnivName() {
	return new QualifiedName(new Id(UNIV), _getLangModuleName(UNIV));
    }

    /**@return fully qualified name of Signature Int  **/
    private static QualifiedName _getIntName() {
	return new QualifiedName(new Id(INT), _getLangModuleName(INT));
    }
    
    /**
     * If alloy/lang/Int has not already been imported by some other module,
     * adds it _lang.  If alloy/lang/Int has not already been imported by
     * the current module, its name is added to _importedLangModules
     **/
    private void _importInt() {
	if (!_importedLangModules.hasChild(_getLangModuleName(INT))) // Int is lazily imported
	    _importedLangModules.addQualifiedName(_getLangModuleName(INT));
	if (_lang.numChildren() == 1) // virtual Int module is lazily created
	    _lang.addModule(_getIntModule((Module) _lang.getModuleIter().next()));
	
    }


    /****************************************************************
     *                   TOP LEVEL STUFF                            *
     *  SpecificationCST    => Specification                        *
     *  ModuleCST           => Modules                              *
     *  ImportCST           => QualifiedNames                       *
     *  ModulePathCST       => QualifiedNames                       *
     *                                                              *
     ****************************************************************/

    /**
     * visits the SpecificationCST node
     * Fields:
     * <PRE>
     * moduleCST -> ModuleCST()
     * </PRE>
     * @param specificationCST_ the top level node of the CST
     * @param argu_ AlloyParser object used to obtain <code>specificationCST_</code>
     * @return AST {@link Specification}
     */
    public Object visit(SpecificationCST specificationCST_, Object argu_) {
    	final AlloyPrepass.ParserNames names = (AlloyPrepass.ParserNames) argu_;
        _signatureNames = names.signatureNames;
	Modules open = (Modules) specificationCST_.moduleCST.accept(this, null);
        Module topModule = (Module) open.getModuleIter().next();
	//System.out.println(topModule + " : "+ _parsedModules);
	
	if (topModule.getName().equals(_parsedModules.get(0))) {
         //	 if this is the final spec, add alloy/lang to its modules:
	    Modules temp = new Modules(open.getLocation());
	    temp.addModules(_lang);
	    temp.addModules(open);
	    open = temp;
         // also, if the virtual alloy/lang/Int module was transtively opened,
	    // it should be added to the list of opened modules in the top module
	    if (!topModule.getOpenedModules().hasChild(_getLangModuleName(INT)) &&
	         _lang.numChildren() == 2) {
	        topModule.getOpenedModules().addQualifiedName(_getLangModuleName(INT));
	    }
	}


/**
        println(true, _currentModuleName + "'s openings:");
        for(Iterator i = topModule.getOpenedModules().getQualifiedNameIter(); i.hasNext();) {
            println(true, i.next()); 
        }
**/
        
        return new Specification(topModule.getLocation(), topModule, _lang, open, names);
    }

    /**
     * visits the ModuleCST node
     * Fields:
     * <PRE>
     * moduleDeclCST -> ModuleDeclCST()
     * nodeListOptional -> ( ImportCST() )*
     * nodeListOptional1 -> ( ParagraphCST() )*
     * nodeToken -> &lt;EOF&gt;
     * </PRE>
     * @param moduleCST_, module node of the CST
     * @param argu_ not used
     * @return AST {@link Modules}
     */
    public Object visit(ModuleCST moduleCST_, Object argu_) {
        Modules modules = new Modules();

        /***********SET MODULE NAME**************************************/

        // new module importing scheme: aliases are transparent
        _currentModuleName  = (QualifiedName) moduleCST_.moduleDeclCST.accept(this, null);
        _environ.setName(_currentModuleName);
	
	println(_debugSwitch, "--------- Parsing " + _currentModuleName + " ----------");
        println(_debugSwitch, "Current Environment: " + _environ);

        /***********GET PARAGRAPHS***************************************/
        Signatures signatures = new Signatures();
        Facts facts = new Facts();
        Predicates predicates = new Predicates();
        Functions functions = new Functions();
        Assertions assertions = new Assertions();
        Commands commands = new Commands();

        QualifiedNames polyParams = new QualifiedNames();

        // if top-level module, create dummy sigs for each typeVar in Environment
        if(_environ.isTopLevel()) {
            Iterator typeVars = _polyTypeVarIds.getIdIter();
            while (typeVars.hasNext()) {
                Id typeVar = (Id)typeVars.next();
                Location location = typeVar.getLocation();
                QualifiedName name = new QualifiedName(location, typeVar, _currentModuleName);

                // create dummy sig
		SigExprs dummyExtends = new SigExprs();
		dummyExtends.addSigExpr(new SigExpr(_getUnivName()));
                Signature sig = new Signature(location, name, dummyExtends, new SigExprs(), new Decls(),
                    new Fact(new QualifiedName(Location.UNKNOWN,
                                                Id.generateId("Fact"),
                                                _currentModuleName)),
                    Multiplicity.SET, false, false);
                signatures.addSignature(sig);
            }
        } else { // not a top-level module, so bind type vars to appropriate type args

            // check the number of import arguments
            if (_environ.getNumTypeArgsToBind() != _polyTypeVarIds.numChildren()) {
                Dbg.user(new Msg("Improper number of arguments for imported module " + _currentModuleName +
                                 ". Expected " + _polyTypeVarIds.numChildren(),
                                 _currentModuleName));
            } else {
                // first, save a copy of all the fully QualifiedNames of polymorphic parameters
                // for use in module creation
                polyParams = _environ.getTypeArgs();//getTypeArgs();
                //println(debugSwitch, "PARSING " + _currentModuleName);
                // bind type vars to type args sequentially
                Iterator typeVars = _polyTypeVarIds.getIdIter();
                while (typeVars.hasNext()) {
                    Id typeVar = (Id) typeVars.next();
		    
                    //_environ.bindVar(typeVar, _curPath);
                    _environ.bindVar(new QualifiedName(typeVar.getLocation(),
						       typeVar,
						       _curPath));
                    /*} catch (PolymorphicCycleException e) {
		      Dbg.user(new Msg("Cycle detected while instantiating " + importName +
		      " with " + typeVar.nodeString(),
		      typeVar));
		      }*/
                }



            }
        }

	println(_debugSwitch, "Environment after binding:" + _environ);
	
	/*********** GET IMPORTED MODULES ***************************/
	
	Enumeration imports = moduleCST_.nodeListOptional.elements();
	ImportCST moduleImport;
	QualifiedNames opens = new QualifiedNames();
	QualifiedNames uses = new QualifiedNames();
	
	Map namesToEnviron = new HashMap(); // Module's QualifiedName -> Environment
	
	Set importedNames = new HashSet();
        
	while (imports.hasMoreElements()) {
	    // need to check whether:
	    // 1- non-parameterized module imported more than once
	    // 2- conflicting names: ie. duplicate aliases or duplicate import of
	    //		of parameteric module without alias
	    
	    // to do this, 
	    // store all names in importedNames, with parameters if they exist 
	    Environment subEnvironment = _environ.extend();
	    
	    moduleImport = (ImportCST) imports.nextElement();
	    
	    // does the import statement have an alias?
	    //boolean hasAlias = moduleImport.nodeOptional1.present();
	    
	    // sets importedModule to module name, or alias if one exists
	    // also binds alias to module name in _aliasesToModuleNames
	    QualifiedName importedModule = (QualifiedName)moduleImport.accept(this,subEnvironment);
	    
	    println(_debugSwitch, "Imported Module: " + importedModule);
	    //System.out.println("Imported Module Path: " + importedModuleName.getPath());
	    //System.out.println("Imported Module Path Hash: " + importedModuleName.getPath().hashCode());
	    //System.out.println("Imported Module Id: " + importedModuleName.getId());
	    //System.out.println("Imported Module Id Hash: " + importedModuleName.getId().hashCode());
	    //System.out.println("Imported Module Hash: " + importedModuleName.hashCode());
	    
	    
	    
	    if (importedNames.contains(importedModule)) {
		ModuleId id = (ModuleId)importedModule.getId();
		// importedModule.getId() instanceof ModuleId
		if(id.hasNoTypeParams()) {
		    Dbg.user(new Msg("Module cannot be imported more than once: " +
				     importedModule,
				     importedModule));
		} else {
		    Dbg.user(new Msg("Parameterized module cannot be re-instantiated with same set of sigs: " + 
				     importedModule,
				     importedModule));
		}
	    } else {
		importedNames.add(importedModule);
	    }
			 
	    // bind alias or module name to environment
	    // note: importedModule of type QualifiedName
	    namesToEnviron.put(importedModule, subEnvironment);
	    /*
	      if (_aliasesToModuleNames.containsKey(importedModule)) {
	      QualifiedName actualName = (QualifiedName)_aliasesToModuleNames.get(importedModule);
	      opens.addQualifiedName(actualName);
	      } else {
	    */
	    /**
	    if(moduleImport.nodeOptional1.present()) {
		uses.addQualifiedName(importedModule);
	    } else {
	    **/
	    /** EMINA:  we now open everything to ensure that
	     * aliases are really just that (i.e. you can still
	     * refer to a sig in a module opened with an alias
	     * by its fully qualified name **/
	    opens.addQualifiedName(importedModule);
	    //}
	    
	    //}
	    
	}

        Enumeration paragraphs = moduleCST_.nodeListOptional1.elements();
        while (paragraphs.hasMoreElements()) {
            alloy.parse.syntaxtree.Node paragraph =
                ((ParagraphCST) paragraphs.nextElement()).nodeChoice.choice;

            // depending on the type of each paragraph, add the paragraph to the appropriate
            // AST sequence node
            if (paragraph instanceof SignatureCST) {
                signatures.addSignatures((List) (paragraph.accept(this, null)));
            }
            if (paragraph instanceof FactCST) {
                facts.addFact((Fact) (paragraph.accept(this, null)));
            }
            if (paragraph instanceof PredicateCST) {
                predicates.addPredicate((Predicate) (paragraph.accept(this, null)));
            }
            if (paragraph instanceof FunctionCST) {
                functions.addFunction((Function) (paragraph.accept(this, null)));
            }
            if (paragraph instanceof AssertionCST) {
                assertions.addAssertion((Assertion) (paragraph.accept(this, null)));
            }
            if (paragraph instanceof RunCST) {
                commands.addCommand((RunCommand) (paragraph.accept(this, null)));
            }
            if (paragraph instanceof CheckCST) {
                commands.addCommand((CheckCommand) (paragraph.accept(this, null)));
            }
        }

        // DEBUGGING


        /*
        Iterator sigIter = signatures.getSignatureIter();
        println(debugSwitch, "Sigs: ");
        while (sigIter.hasNext()) {
            println(debugSwitch, "\t" + sigIter.next());
        }
        */



        /* Location bounded by
         * "module" = moduleCST_.moduleDeclCST.nodeToken and
         * "EOF" = moduleCST_.nodeToken*/

	// add the opened modules to alloy/lang modules that are imported by default;
	// we don't do the reverse (adding lang modules to opened module) so that we 
	// don't need to worry about accidental "parsing" of lang modules (see the code
	// below which parses the imported modules)
	_importedLangModules.addQualifiedNames(opens);
        Module newModule =
            new Module(
                new Location(
                    _fileName,
                    moduleCST_.moduleDeclCST.nodeToken,
                    moduleCST_.nodeToken),
                _currentModuleName,
                signatures,
                facts,
                predicates,
                functions,
                assertions,
                commands,
                uses,
                _importedLangModules,      // sharing mode?
                polyParams);

        newModule.setAliasMappings(_aliasesToModuleNames);
        modules.addModule(newModule);

    /** DEBUGGING **/

        String polyParamsString = "";
        if (polyParams.numChildren() == 0) {
            polyParamsString += "none";
        } else {
            for (Iterator i = polyParams.getQualifiedNameIter(); i.hasNext();) {
                polyParamsString += i.next().toString() + " ";
            }
        }
        //System.out.println("PolyParams of " + _currentModuleName + ": " + polyParamsString);

        // this module has been parsed
        _parsedModules.add(_currentModuleName);
        
        // store the unparameterized module name for cycle detection
        QualifiedName unparameterizedModuleName;
        unparameterizedModuleName = new QualifiedName(_currentModuleName.getLocation(),
						      new Id(_currentModuleName.getId().getLocation(),
							     ((ModuleId)_currentModuleName.getId()).unparameterizedNodeString()),
						      _currentModuleName.getPath());
        _importCycles.add(unparameterizedModuleName);

        //println(_debugSwitch, "_parsedModules: " + _parsedModules);
        //println(_debugSwitch, "_importCycles: " + _importCycles);


        /***********PARSE ALL THE OTHER MODULES**************************/
        //println(debugSwitch, "Going into other modules...");
		QualifiedNames importNames = new QualifiedNames();
        importNames.addQualifiedNames(opens);
        importNames.addQualifiedNames(uses);
        Iterator importedModules = importNames.getQualifiedNameIter();

	//System.out.println("*****");
	//System.out.println(unparameterizedModuleName);
	//System.out.println(_importCycles);
	//System.out.println("*****");

        while (importedModules.hasNext()) {
            // retrieves fully qualified name of module
            QualifiedName moduleName = (QualifiedName) importedModules.next();
            
	    unparameterizedModuleName = new QualifiedName(moduleName.getLocation(),
							  new Id(moduleName.getId().getLocation(),
								 ((ModuleId)moduleName.getId()).unparameterizedNodeString()),
							  moduleName.getPath());
	    println(_debugSwitch, "Unparameterized import module name: " + unparameterizedModuleName);
	    // cycle detection
	    if (_importCycles.contains(unparameterizedModuleName)) {
		Dbg.user(new Msg("Cycle detected in import graph",
				 moduleName));
		continue;
	    }
	    
	    /** EMINA:  THIS DOESN'T WORK.  SEE THE FIX BELOW ***/
	    // add the name even though the parse of the module will add it again
	    // prevents infinite loops of the following form:
	    //
	    // module M
	    // open D/M
	    //_importCycles.add(unparameterizedModuleName);
            if (!_parsedModules.contains(moduleName)) {
                //parse file
                File file = null;

                //println(debugSwitch, "namesToEnviron: " + namesToEnviron);
                Environment env = (Environment)namesToEnviron.get(moduleName);
                //println(debugSwitch, "name of next module to parse: " + moduleName);
                //println(debugSwitch, "env from map: " + env);

/*
                // handler for imports with aliases
                if(_aliasesToModuleNames.containsKey(moduleName)) {
                    // instantiate with alias, but check for file with real name
                    QualifiedName alias = moduleName;
                    moduleName = (QualifiedName) _aliasesToModuleNames.get(moduleName);
                }
*/
                //println(debugSwitch, "actual moduleName: " + moduleName);

                try {

                    file = FileUtil.getModuleFile(moduleName.getPath().nodeString() + "/" + ((ModuleId) moduleName.getId()).unparameterizedNodeString());
                } catch (FileNotFoundException e) {
                    Dbg.user(
                        new Msg(
                            "File for module " + moduleName.nodeString() +
                               " not found in module path " +
                               FileUtil.getModulePath().replaceAll(";\\.", "/"),
                            moduleName));
                    return modules;
                }
		/** EMINA:  THE FOLLOWING THREE LINES PREVENT IMPORT CYCLES **/
		Set importCyclesCopy = new HashSet(_importCycles);
		importCyclesCopy.add(unparameterizedModuleName);
                Specification spec = MakeASTVisitor._getAST(file, _parsedModules, importCyclesCopy, env, _lang);
                if (spec == null) {
                    return modules;
                } else {
                    // check that module was opened with proper name
                    //QualifiedName realModuleName2 = spec.getFocus().getName();
                    QualifiedName realModuleName = env.getName();
                    println(_debugSwitch, "moduleName: " + moduleName);
                    println(_debugSwitch, "realModuleName: " + realModuleName);
                    
		    /*
		    boolean moduleMatch;
		    if (!realModuleName.getPath().equals(moduleName.getPath())) {
			moduleMatch = false;
		    } else if (realModuleName.getId() instanceof ModuleId && moduleName.getId() instanceof ModuleId) {
			moduleMatch = ((ModuleId)realModuleName.getId()).similarTo(moduleName.getId());
		    } else if (realModuleName.getId() instanceof Id && moduleName.getId() instanceof Id) {
			moduleMatch = realModuleName.getId().equals(moduleName.getId());
		    } else {
			moduleMatch = false;
		    }

                    if (!moduleMatch) {
		    */
		    if (!realModuleName.equals(moduleName)) {
                    	println(_debugSwitch, "Imported Module Name: " + moduleName);
		        println(_debugSwitch, "Imported Module Path: " + moduleName.getPath());
			println(_debugSwitch, "Imported Module Path Hash: " + moduleName.getPath().hashCode());
		        println(_debugSwitch, "Imported Module Id: " + moduleName.getId());
			println(_debugSwitch, "Imported Module Id Name: " + moduleName.getId().getName());
						
			println(_debugSwitch, "Imported Module Id Hash: " + moduleName.getId().hashCode());
			println(_debugSwitch, "Imported Module Hash: " + moduleName.hashCode());
			println(_debugSwitch, "Environment Module Name: " + realModuleName);
			println(_debugSwitch, "Environment Module Path: " + realModuleName.getPath());
			println(_debugSwitch, "Environment Module Path Hash: " + realModuleName.getPath().hashCode());
			println(_debugSwitch, "Environment Module Id: " + realModuleName.getId());
			println(_debugSwitch, "Environment Module Id Name: " + realModuleName.getId().getName());
			println(_debugSwitch, "Environment Module Id Hash: " + realModuleName.getId().hashCode());
			println(_debugSwitch, "Environment Module Hash: " + realModuleName.hashCode());
			println(_debugSwitch, "Path.equals() " + moduleName.getPath().equals(realModuleName.getPath()));
			println(_debugSwitch, "Id.equals() " + moduleName.getId().equals(realModuleName.getId()));
			
			Dbg.user(new Msg("Name of module does not match location",
					 moduleName));
			
                        return modules;
                    } else {
                        //add to modules
                        modules.addModules(spec.getModules());
                    }
                }
            }
        }

        println(_debugSwitch, "Alloy parse of " + _currentModuleName + " complete.");
        return modules;

    }

    /**
     * <PRE>
     * nodeToken -> &lt;OPEN&gt;
     * nodeOptional -> [ ModulePathCST() ]
     * moduleNameCST -> ModuleNameCST()
     * nodeOptional1 -> [ TypeArgsCST() ]
     * nodeOptional2 -> [ &lt;AS&gt; AliasCST() ]
     * </PRE>
     * @param importCST_, import node of the CST
     * @param argu_ Environment for imported module
     * @return AST {@link QualifiedNames} the moduleName
     */
    public Object visit(ImportCST importCST_, Object argu) {

        QualifiedNames typeArgs = new QualifiedNames();

        //polymorphic?
        if(importCST_.nodeOptional1.present()) {
            // visit the TypeArgsCST
            // stores args in environment for future binding
            typeArgs = (QualifiedNames)importCST_.nodeOptional1.node.accept(this, argu);

        }

	Path modulePath = (importCST_.nodeOptional.present() ?
			   (Path) importCST_.nodeOptional.node.accept(this,null) : 
			   new Path());

	Id moduleId = (Id) importCST_.moduleNameCST.accept(this, typeArgs);
	
	Location nameLocation = (modulePath.isLeaf() ? moduleId.getLocation() : 
				 new Location(modulePath, moduleId));
	
	QualifiedName moduleName = new QualifiedName(nameLocation, moduleId, modulePath);
	

        // alias?
        if(importCST_.nodeOptional2.present()) {
            Enumeration aliasSequence = ((NodeSequence)importCST_.nodeOptional2.node).elements();
            aliasSequence.nextElement();
            QualifiedName aliasName = (QualifiedName)((AliasCST)aliasSequence.nextElement()).accept(this,typeArgs);

            //println(debugSwitch, "Import's PackageSpecifierPath = " + ((QualifiedName)actualName.getQualifiedNameIter().next()).getPath());

            // store a mapping from aliasName to moduleName for polymorphism
            _aliasesToModuleNames.put(aliasName, moduleName);
            //System.out.println("importCST _aliasesToModuleNames: " + _aliasesToModuleNames);
        } 
        
        // no alias
        return moduleName;
    }


    /****************************************************************
     *                   PARAGRAPH STUFF                            *
     *  SignatureCST  => Signature                                  *
     *  FactCST       => Fact                                       *
     *  PredicateCST  => Predicate                                  *
     *  FunctionCST   => Function                                   *
     *  AssertionCST  => Assertion                                  *
     *  ExtensionCST  => Ids  NOT DONE                              *
     *  FormulaSeqCST => FormulaSeq                                 *
     *                                                              *
     ****************************************************************/

    /**
     * <PRE>
     * nodeOptional -> [ MultCST() ]
     * nodeListOptional -> ( SigQualCST() )*
     * nodeToken -> &lt;SIG&gt;
     * nodeToken1 -> &lt;ID&gt;
     * nodeListOptional1 -> ( &lt;COMMA&gt; &lt;ID&gt; )*
     * nodeOptional1 -> [ ExtensionCST() ]
     * nodeToken2 -> &lt;LBRACE&gt;
     * nodeOptional2 -> [ DeclCST() ( &lt;COMMA&gt; DeclCST() )* ]
     * nodeToken3 -> &lt;RBRACE&gt;
     * nodeOptional3 -> [ FormulaSeqCST() ]
     * </PRE>
     * @param signatureCST_, signature node of the CST
     * @param argu_ not used
     * @return {@link List} of {@link Signature signatures}
     */
    public Object visit(SignatureCST signatureCST_, Object argu_) {

    /***********GET LOCATION*****************************************/
        /* Location bounded by "sig" and "}"*/
        Location location = new Location(_fileName,
                     signatureCST_.nodeToken,
                     signatureCST_.nodeToken3);

    /***********GET MULTIPLICITY ************************************/
    Multiplicity mult;
    if (signatureCST_.nodeOptional.present()) { // multiplicity specified . . .
        mult = (Multiplicity)
                   ((MultCST) signatureCST_.nodeOptional.node).accept(this, null);

    } else { // the implied multiplicity is SET
        mult = Multiplicity.SET;
    }

        /***********GET QUALIFIERS***************************************/
        boolean isProduct = false;
        boolean isAbstract = false;

        if (signatureCST_.nodeListOptional.present()) {
            for (Enumeration enum2 = signatureCST_.nodeListOptional.elements();
                enum2.hasMoreElements();
                ) {
                SigQualCST sigQualifier = (SigQualCST) enum2.nextElement();
                int qualNum = sigQualifier.nodeChoice.which;
        Location qualifierLoc = new Location(_fileName,
                             (NodeToken) sigQualifier.nodeChoice.choice);
                switch (qualNum) {
                    case 0 : // <ABSTRACT>
            if (isAbstract) { // if already encountered, signal an error
                error("abstract already specified", new DummyNode(qualifierLoc));
            }
                        isAbstract = true;
                        break;
                    case 1 : // <PRODUCT>
            if (isProduct) { // if already encountered, signal an error
                error("product already specified", new DummyNode(qualifierLoc));
            }
                        isProduct = true;
                        break;
                    default :
                        Dbg.chk(false);
                }
            }
        }

        /***********GET NAME*********************************************/
        Location tokenLocation =
            new Location(_fileName, signatureCST_.nodeToken1);
        QualifiedName name =
            new QualifiedName(
                tokenLocation,
                new Id(tokenLocation, signatureCST_.nodeToken1.tokenImage),
                _currentModuleName);

        /***********CHECK FOR SIG NAME SHADOWING*************************/
        noShadow(name.getId());

        /***********GET EXTENDS SIGEXPR / IN SUBSETEXPR**************************************/
        SigExprs extendsExprs = new SigExprs();
        SigExprs subsetsExprs = new SigExprs();
        boolean doesExtend = signatureCST_.nodeOptional1.present();
        if (doesExtend) {
            // node has type ExtensionsCST
            Object ret = signatureCST_.nodeOptional1.node.accept(this, null);

            if (((ExtensionCST) signatureCST_.nodeOptional1.node)
                .nodeChoice
                .which
                == 0) { // sig created using "extends"
                extendsExprs = (SigExprs) ret;
            } else { // sig created using "in"
		subsetsExprs = (SigExprs) ret;
            }
        } else { // implicitly extends univ
	    extendsExprs.addSigExpr(new SigExpr(_getUnivName()));
	}

        /***********GET DECLARATIONS*************************************/
        Decls decls = new Decls();
        if (signatureCST_.nodeOptional2.present()) {
            // get the sequence of decls
            Enumeration declSequence =
                ((NodeSequence) signatureCST_.nodeOptional2.node).elements();
            decls = createDecls(declSequence);
        }

        /***********GET FACT*********************************************/
        Fact fact =
            new Fact(
                new QualifiedName(
                    Location.UNKNOWN,
                    Id.generateId("Fact"),
                    _currentModuleName));
        if (signatureCST_.nodeOptional3.present()) {
            // get the formula sequence of the fact
            FormulaSeq formulaSeq =
                (FormulaSeq) signatureCST_.nodeOptional3.node.accept(
                    this,
                    null);
            // construct fact with same type param ids as signature for uniformity
            fact =
                new Fact(
                    formulaSeq.getLocation(),
                    fact.getName(),
                    formulaSeq);
        }

        // product sig cannot have multiplicity one or lone
        if (isProduct && (mult.equals(Multiplicity.ONE) || mult.equals(Multiplicity.LONE)))
            error(
                "product signature cannot have multiplicity " + mult.nodeString(),
                mult);

        // can't extend another sig if declared a product
        if (doesExtend && isProduct) {
        if (extendsExprs.getSigExprIter().hasNext()) {
        error(
              "product signatures cannot extend another signature",
              extendsExprs);
        } else {
        error(
              "product signatures cannot subset another signature",
              subsetsExprs);
        }
        }

        // can't have abstract and subsetExpr
        if (isAbstract && subsetsExprs.getSigExprIter().hasNext()) {
            error(
                "abstract signature must be a type",
                subsetsExprs);
        }


        List signatures = new ArrayList();
        Signature sig =
            new Signature(
                location,
                name,
                extendsExprs,
                subsetsExprs,
                decls,
                fact,
                mult,
                isProduct,
                isAbstract);
        signatures.add(sig);

        /***********GET OTHER SIGNATURE NAMES****************************/
        Enumeration otherSigs = signatureCST_.nodeListOptional1.elements();
        // make sure no fields were declared if there are multiple sig names
        if (otherSigs.hasMoreElements()
            && signatureCST_.nodeOptional2.present()) {
            error(
                "no field declarations allowed with multiple signature names",
                decls);
        }

        while (otherSigs.hasMoreElements()) {
            NodeSequence nodeSeq = (NodeSequence) otherSigs.nextElement();
            NodeToken nodeToken = (NodeToken) nodeSeq.elementAt(1);
            tokenLocation = new Location(_fileName, nodeToken);
            name =
                new QualifiedName(
                    tokenLocation,
                    new Id(tokenLocation, nodeToken.tokenImage),
                    _currentModuleName);
            // make sure that type params are the same
            Fact otherFact =
                new Fact(
                    fact.getLocation(),
                    new QualifiedName(
                        Id.generateId("Fact"),
                        _currentModuleName),
                    (FormulaSeq) fact.getFormula().copy());
            Signature otherSig =
                new Signature(
                    location,
                    name,
                    extendsExprs,
                    subsetsExprs,
                    decls,
                    otherFact,
                    (Multiplicity)mult.copy(),
                    isProduct,
                    isAbstract);
            signatures.add(otherSig);
        }

        return signatures;
    }

    /**
     * <PRE>
     * nodeToken -> &lt;FACT&gt;
     * nodeOptional -> [ &lt;ID&gt ]
     * formulaSeqCST -> FormulaSeqCST()
     * </PRE>
     * @param factCST_, fact node of the CST
     * @param argu_ not used
     * @return AST {@link Fact}
     */
    public Object visit(FactCST factCST_, Object argu_) {

        /***************GET NAME*************************/
        QualifiedName name;
        // if name is declared, get it
        if (factCST_.nodeOptional.present()) {
            name =
                new QualifiedName(
                    new Location(
                        _fileName,
                        (NodeToken) factCST_.nodeOptional.node),
                    new Id(
                        new Location(
                            _fileName,
                            (NodeToken) factCST_.nodeOptional.node),
                        ((NodeToken) factCST_.nodeOptional.node).tokenImage),
                    _currentModuleName);
        } else {
            name =
                new QualifiedName(
                    Location.UNKNOWN,
                    Id.generateId("Fact"),
                    _currentModuleName);
        }
        /**************GET FORMULA SEQUENCE**************/
        FormulaSeq formulaSeq =
            (FormulaSeq) factCST_.formulaSeqCST.accept(this, null);

        /***************GET LOCATION*********************/
        Location location = new Location(factCST_.nodeToken, formulaSeq);

        // location is from assertionCST_.nodeToken = "fact" to
        // end of formula sequence = "}"
        return new Fact(location, name, formulaSeq);

    }

    /**
     * <PRE>
     * nodeToken -> &lt;PRED&gt;
     * nodeOptional -> [ SigCST() ( &lt;DOT&gt; | &lt;DOUBLECOLON&gt; ) ]
     * nodeToken1 -> &lt;ID&gt;
     * nodeToken2 -> &lt;LPAREN&gt;
     * nodeOptional1 -> [ DeclCST() ( &lt;COMMA&gt; DeclCST() )* ]
     * nodeToken3 -> &lt;RPAREN&gt;
     * formulaSeqCST -> FormulaSeqCST()
     * </PRE>
     * @param predicateCST_, predicate node of the CST
     * @param argu_ not used
     * @return AST {@link Predicate}
     */
    public Object visit(PredicateCST predicateCST_, Object argu_) {

        /***********GET NAME*********************************************/
        QualifiedName name =
            new QualifiedName(
                new Location(_fileName, predicateCST_.nodeToken1),
                new Id(
                    new Location(_fileName, predicateCST_.nodeToken1),
                    (predicateCST_.nodeToken1.tokenImage)),
                _currentModuleName);

        /***********GET RECEIVER DECLARATION*****************************/
        Decl receiverDecl = new Decl();
        // if a receiver is declared, create a Decl node for it
        if (predicateCST_.nodeOptional.present()) {
            // will be a node sequence with SigCST() node as first in sequence
            // get SigExpr for it
            SigExpr sigReceiverExpr =
                (SigExpr) ((NodeSequence) predicateCST_.nodeOptional.node).elementAt(0).accept(
                    this,
                    null);
            Location sigExprLoc = sigReceiverExpr.getLocation();
            // create "this" variable
            Variables vars = new Variables();
            vars.addVariable(
                new Variable(new Id(Location.UNKNOWN, "this")));
            receiverDecl =
                new Decl(
                    sigExprLoc,
                    new Qualifiers(),
                    vars,
                    new SetMultExpr(sigExprLoc, Multiplicity.NONE, sigReceiverExpr));
        }

        /***********GET MAIN DECLARATIONS********************************/
        Decls mainDecls = new Decls();
        // if arguments are declared, get their Decls
        if (predicateCST_.nodeOptional1.present()) {
            // get enumeration of decls from NodeSequence
            Enumeration declSequence =
                ((NodeSequence) predicateCST_.nodeOptional1.node).elements();
            mainDecls = createDecls(declSequence);
        }
	//mainDecls.setLocation(predicateCST_.nodeToken2, predicateCST_.nodeToken3);

        /***********GET FORMULA SEQUENCE ***************************************/
        FormulaSeq formula = (FormulaSeq)predicateCST_.formulaSeqCST.accept(this, null);

        /***********GET LOCATION*****************************************/
        // location is from beginning of predicateCST_.nodeToken = "pred" to end of
        // formula sequence = "}"
        Location location = new Location(predicateCST_.nodeToken, formula);

        return new Predicate (
            location,
            name,
            formula,
            new ArgList(Location.UNKNOWN, receiverDecl, mainDecls));
    }

    /**
     * <PRE>
     * nodeToken -> &lt;FUN&gt;
     * nodeOptional -> [ SigCST() ( &lt;DOT&gt; | &lt;DOUBLECOLON&gt; ) ]
     * nodeToken1 -> &lt;ID&gt;
     * nodeToken2 -> &lt;LPAREN&gt;
     * nodeOptional1 -> [ DeclCST() ( &lt;COMMA&gt; DeclCST() )* ]
     * nodeToken3 -> &lt;RPAREN&gt;
     * nodeToken4 -> &lt;COLON&gt;
     * multExprCST -> MultExprCST()
     * nodeToken5 -> &lt;LBRACE&gt;
     * exprCST -> ExprCST()
     * nodeToken6 -> &lt;RBRACE&gt;
     * </PRE>
     * @param functionCST_, function node of the CST
     * @param argu_ not used
     * @return AST {@link Function}
     */
    public Object visit(FunctionCST functionCST_, Object argu_) {

        /***********GET RECEIVER DECLARATION*****************************/
        Decl receiverDecl = new Decl();
        // if a receiver is declared, create a Decl node for it
        if (functionCST_.nodeOptional.present()) {
            // will be a node sequence with SigCST() node as first in sequence
            // get SigExpr for it
            SigExpr sigReceiverExpr =
                (SigExpr) ((NodeSequence) functionCST_.nodeOptional.node).elementAt(0).accept(
                    this,
                    null);
            Location sigExprLoc = sigReceiverExpr.getLocation();
            // create "this" variable
            Variables vars = new Variables();
            vars.addVariable(new Variable(new Id(Location.UNKNOWN, "this")));
            receiverDecl =
                new Decl(
                    sigExprLoc,
                    new Qualifiers(),
                    vars,
                    new SetMultExpr(
                        sigExprLoc,
                        Multiplicity.NONE,
                        sigReceiverExpr));
        }

        /***********GET NAME*********************************************/
        QualifiedName name =
            new QualifiedName(
                new Location(_fileName, functionCST_.nodeToken1),
                new Id(
                    new Location(_fileName, functionCST_.nodeToken1),
                    (functionCST_.nodeToken1.tokenImage)),
        _currentModuleName);


        /***********GET MAIN DECLARATIONS********************************/
        Decls mainDecls = new Decls();
        // if arguments are declared, get their Decls
        if (functionCST_.nodeOptional1.present()) {
            // get enumeration of decls from NodeSequence
            Enumeration declSequence =
                ((NodeSequence) functionCST_.nodeOptional1.node).elements();
            mainDecls = createDecls(declSequence);
        }

        /***********GET RETURN EXPRESSION********************************/
        MultiplicityExpr returnExpr =
            (MultiplicityExpr) functionCST_.multExprCST.accept(this, null);

        /***********GET EXPRESSION***************************************/
        Expr expr = (Expr)functionCST_.exprCST.accept(this, null);

        /***********GET LOCATION*****************************************/
        // location is from beginning of functionCST_.nodeToken = "fun" to end of
        // formula sequence = "}"
        Location location = new Location(functionCST_.nodeToken, expr);

        return new Function(
            location,
            name,
            expr,
            new ArgList(Location.UNKNOWN, receiverDecl, mainDecls),
            returnExpr);
    }

    /**
     * visits the AssertionCST node
     * Fields:
     * <PRE>
     * nodeToken -> &lt;ASSERT&gt;
     * nodeOptional -> [ &lt;ID&gt ]
     * formulaSeqCST -> FormulaSeqCST()
     * @param assertionCST_, assertion node of the CST
     * @param argu_ not used
     * @return AST {@link Assertion}
     */
    public Object visit(AssertionCST assertionCST_, Object argu_) {

        /***************GET NAME*************************/
        QualifiedName name;
        // if name is declared, get it
        if (assertionCST_.nodeOptional.present()) {
            name =
                new QualifiedName(
                    new Location(
                        _fileName,
                        (NodeToken) assertionCST_.nodeOptional.node),
                    new Id(
                        new Location(
                            _fileName,
                            (NodeToken) assertionCST_.nodeOptional.node),
                        (
                            (
                                NodeToken) assertionCST_
                                    .nodeOptional
                                    .node)
                                    .tokenImage),
                    _currentModuleName);
        } else {
            name =
                new QualifiedName(
                    Location.UNKNOWN,
                    Id.generateId("Assert"),
                    _currentModuleName);
        }

        /**************GET FORMULA SEQUENCE**************/
        FormulaSeq formulaSeq =
            (FormulaSeq) assertionCST_.formulaSeqCST.accept(this, null);

        /***************GET LOCATION*********************/
        // location is from assertionCST_.nodeToken = "assert" to
        // end of formula sequence = "}"
        Location location = new Location(assertionCST_.nodeToken, formulaSeq);

        return new Assertion(location, name, formulaSeq);
    }

    /**
     * <PRE>
     * nodeToken -> &lt;LBRACKET&gt;
     * typeArgCST -> TypeArgCST()
     * nodeListOptional -> ( &lt;COMMA&gt; TypeArgCST() )*
     * nodeToken1 -> &lt;RBRACKET&gt;
     * </PRE>
     * @param typeArgsCST_, Type Args node of the CST
     * @param argu_ Environment of the imported module
     * @return AST {@link Ids}
     */
    public Object visit(TypeArgsCST typeArgsCST_, Object argu_) {
        /***********GET LOCATION*****************************************/
        Location location =
            new Location(_fileName, typeArgsCST_.nodeToken, typeArgsCST_.nodeToken1);

        /***********GET TYPE ARGUMENTS***********************************/
        // used to keep track of duplicate type arguments
        Set argsSoFar = new HashSet();

        QualifiedNames typeArgs = new QualifiedNames(location);
        QualifiedName nextArg = (QualifiedName)typeArgsCST_.typeArgCST.accept(this, argu_);
        typeArgs.addQualifiedName(nextArg);
        argsSoFar.add(nextArg);

        Enumeration otherTypeArgs = typeArgsCST_.nodeListOptional.elements();

        while (otherTypeArgs.hasMoreElements()) {
            // get the name
            nextArg = (QualifiedName) ((NodeSequence) otherTypeArgs.nextElement()).elementAt(1).accept(this, argu_);
            if(argsSoFar.contains(nextArg)) {
                Dbg.user(new Msg("Duplicate type arguments supplied to import statement: " +
                                 nextArg, nextArg));
            }

            typeArgs.addQualifiedName(nextArg);
        }


        return typeArgs;
    }

    /**
     * <PRE>
     * nodeToken -> &lt;LBRACKET&gt;
     * typeVarCST -> TypeVarCST()
     * nodeListOptional -> ( &lt;COMMA&gt; TypeVarCST() )*
     * nodeToken1 -> &lt;RBRACKET&gt;
     * </PRE>
     * @param typeVarsCST_, Type Vars node of the CST
     * @param argu_ not used
     * @return AST {@link Ids}
     */
    public Object visit(TypeVarsCST typeVarsCST_, Object argu_) {
        /***********GET LOCATION*****************************************/
        Location location =
            new Location(_fileName, typeVarsCST_.nodeToken, typeVarsCST_.nodeToken1);

        /***********GET TYPE VARIALBLES***********************************/
        Ids typeVars = new Ids(location);
        typeVars.addId((Id) typeVarsCST_.typeVarCST.accept(this, null));

        Enumeration otherTypeVars = typeVarsCST_.nodeListOptional.elements();
        while (otherTypeVars.hasMoreElements()) {
            Id typeVar = (Id) ((NodeSequence)
                                  otherTypeVars.nextElement()).elementAt(1).accept(
                                    this,
                                    null);
            if(typeVars.hasChild(typeVar)) {
                Dbg.user(new Msg("Duplicate type variable " + typeVar, typeVar));
            }

            // get the Id
            typeVars.addId(typeVar);
        }

        return typeVars;
    }

    /**
     * <PRE>
     * nodeToken -> &lt;LBRACKET&gt;
     * typeParameterCST -> TypeParameterCST()
     * nodeListOptional -> ( &lt;COMMA&gt; TypeParameterCST() )*
     * nodeToken1 -> &lt;RBRACKET&gt;
     * </PRE>
     * @param typeParemetersCST_, Type Parameters node of the CST
     * @param argu_ not used
     * @return AST {@link QualifiedNames}
     */
    public Object visit(TypeParametersCST typeParametersCST_, Object argu_) {
        /***********GET LOCATION*****************************************/
        Location location =
            new Location(_fileName, typeParametersCST_.nodeToken, typeParametersCST_.nodeToken1);

        /***********GET TYPE ARGUMENTS***********************************/
        QualifiedNames typeParams = new QualifiedNames(location);
        typeParams.addQualifiedName((QualifiedName) 
				    typeParametersCST_.typeParameterCST.accept(this, argu_));

        Enumeration otherTypeParams = typeParametersCST_.nodeListOptional.elements();
        while (otherTypeParams.hasMoreElements()) {
            // get the Id
            typeParams.addQualifiedName((QualifiedName) 
	       ((NodeSequence) otherTypeParams.nextElement()).elementAt(1).accept(
		this,
                argu_));
        }

        return typeParams;
    }

    /**
     * <PRE>
     * <PRE>
     * nodeChoice -> &lt;EXTENDS&gt; SigCST()
     *       | &lt;IN&gt; SigCST() ( &lt;PLUS&gt; SigCST() )*
     * </PRE>
     * @param extensionsCST_, Extensions node of the CST
     * @param argu_ not used
     * @return AST {@link Expr} if a subset, {@link SigExpr} if an extends
     */
    public Object visit(ExtensionCST extensionCST_, Object argu_) {
        SigExprs ret = new SigExprs();
		switch (extensionCST_.nodeChoice.which) {
		case 0: // extends
			// just return the result of converting the SigCST
			Node node = ((NodeSequence) extensionCST_.nodeChoice.choice).elementAt(1);
			SigExpr extendsExpr = (SigExpr) node.accept(this, null);
			ret.addSigExpr(extendsExpr);
			ret.setLocation(extendsExpr.getLocation());
			break;
		case 1: // in
			// we need to create SigExprs
			NodeSequence seq = (NodeSequence) extensionCST_.nodeChoice.choice;

			SigExpr firstSigExpr = (SigExpr) seq.elementAt(1).accept(this, null);
			ret.addSigExpr(firstSigExpr);

			SigExpr lastSigExpr = firstSigExpr;
			NodeListOptional others = (NodeListOptional) seq.elementAt(2);
			for (Enumeration enum2 = others.elements(); enum2.hasMoreElements();) {
				NodeSequence signame = (NodeSequence) enum2.nextElement();
				lastSigExpr = (SigExpr) signame.elementAt(1).accept(this, null);
				ret.addSigExpr(lastSigExpr);
			}
			ret.setLocation(new Location(_fileName,
					firstSigExpr.getLocation().getBeginLine(),
					firstSigExpr.getLocation().getBeginColumn(),
					lastSigExpr.getLocation().getEndLine(),
					lastSigExpr.getLocation().getEndColumn()));
			break;
		}
        return ret;
    }

    /**
	 * <PRE>
	 * 
	 * nodeToken -> &lt;LBRACE&gt; nodeListOptional -> ( FormulaCST() )*
	 * nodeToken1 -> &lt;RBRACE&gt;
	 * 
	 * </PRE>
	 * 
	 * @param formulaSeqCST_,
	 *            Formula Sequence node of the CST
	 * @param argu_
	 *            not used
	 * @return AST {@link FormulaSeq}
	 */
    public Object visit(FormulaSeqCST formulaSeqCST_, Object argu_) {
        /***********GET ID***********************************************/
        Location location =
            new Location(
                _fileName,
                formulaSeqCST_.nodeToken,
                formulaSeqCST_.nodeToken1);

        /***********GET ID***********************************************/
        Enumeration formulaNodes = formulaSeqCST_.nodeListOptional.elements();
        Formulas formulas = new Formulas(location);
		while (formulaNodes.hasMoreElements()) {
			formulas.addFormula((Formula) ((FormulaCST) formulaNodes.nextElement()).accept(this, null));
		}

        return new FormulaSeq(location, formulas);
    }

    /***************************************************************************
	 * NAMES * moduleDeclCST => ModuleName * moduleNameCST => Id *
	 * packageNameCST=> Path * sigNameCST => ParaName * paraNameCST => ParaName *
	 * typeParamCST => Id // not used with polymorphism * typeArgCST => Id *
	 * typeVarCST => Id * *
	 **************************************************************************/

    /**
     * <PRE>
     * nodeToken -> &lt;MODULE&gt;
     * nodeOptional -> [ ModulePathCST() ]
     * moduleNameCST -> ModuleNameCST()
     * nodeOptional1 -> [ TypeVarsCST() ]
     * </PRE>
     * @param moduleDeclCST_, module Declaration node of the CST
     * @param argu_ not used
     * @return AST {@link QualifiedName}
     */
    public Object visit(ModuleDeclCST moduleDeclCST_, Object argu_) {
    /***********GET TYPE VARS****************************************/
        // _polyTypeVarIDs for use in visit to ModuleCST,
        // either for creating dummy sigs or for binding to non top-level envir

        if (moduleDeclCST_.nodeOptional1.present()) {
            // node has type TypeVarsCST
            // store away type variables for environment binding
            _polyTypeVarIds = (Ids)moduleDeclCST_.nodeOptional1.node.accept(this, null);
        }

        /***********GET ID***********************************************/
	QualifiedNames typeArgs = _environ.getFullParameterizedTypeArgs();

    ModuleId id = (ModuleId)
	moduleDeclCST_.moduleNameCST.accept(this, typeArgs);//getTypeArgs());

	println(_debugSwitch, "+++++ Parsing Module Decl - Id: " + id);
	for (Iterator i = typeArgs.getQualifiedNameIter(); i.hasNext();) {
	    println(_debugSwitch, "++ " + i.next());
	}

        /***********GET PATH*********************************************/
        Path path = new Path();
        // used for polymorphic bindings
        _curPath = new Path();

        if (moduleDeclCST_.nodeOptional.present()) {
            //node is of type ModulePathCST
            path = (Path) moduleDeclCST_.nodeOptional.node.accept(this, null);
            _curPath = (Path) moduleDeclCST_.nodeOptional.node.accept(this, null);
        }

        // if alias does not exist, tack on the module name to the path,
        // otherwise, set the path to the alias
        //if(_environ.isTopLevel() || _environ.getImportName().equals(_environ.getRealName())) {
            _curPath.getPackages().addId(id);
        //} else {
        //    _curPath = new Path();
        //    _curPath.getPackages().addId(new Id(Location.UNKNOWN, _environ.getImportName().nodeString()));
        //}

        // new Id(new Location(_fileName, CST.nodeToken), CST.nodeToken.tokenImage);
        //println(debugSwitch, "_curPath: " + _curPath);


        /***********GET LOCATION*****************************************/
        Location location = new Location(path, moduleDeclCST_.moduleNameCST.nodeToken);

        //return new QualifiedName(location, id, path);
        return new QualifiedName(location, id, path);
    }

    /**
    * <PRE>
    * nodeList -> ( DirCST() )+
    * </PRE>
    * @param moduleNameCST_, module Name node of the CST
    * @param argu_ not used
    * @return AST {@link Path}
    */
    public Object visit(ModulePathCST modulePathCST_, Object argu_) {

	/***********GET PACKAGES*****************************************/
        Ids packages = new Ids();
        Enumeration dirNodes = modulePathCST_.nodeList.elements();
        Id firstId = (Id) ((DirCST) dirNodes.nextElement()).accept(this, null);
        packages.addId(firstId);
        Id currentId = firstId;
        while (dirNodes.hasMoreElements()) {
            currentId =
                (Id) ((DirCST) dirNodes.nextElement()).accept(this, null);
            packages.addId(currentId);
        }

	/***********GET LOCATION*****************************************/
        Location location = new Location(firstId, currentId);
	
	return new Path(location, packages);

    }
    /**
     * <PRE>
     * nodeToken -> &lt;ID&gt;
     * </PRE>
     * @param moduleNameCST_, module Name node of the CST
     * @param argu_ {@link QualifiedNames} (type args)
     * @return AST {@link ModuleId}
     */
    public Object visit(ModuleNameCST moduleNameCST_, Object argu_) {
        /***********GET ID***********************************************/
        String id = moduleNameCST_.nodeToken.tokenImage;

        /***********GET LOCATION*****************************************/
        Location location = new Location(_fileName, moduleNameCST_.nodeToken);

    QualifiedNames typeArgs = (argu_ == null ? new QualifiedNames() :
                   (QualifiedNames) argu_);
        return new ModuleId(location, id, typeArgs);
    }

    /**
     * <PRE>
     * nodeChoice -> ModuleNameCST() TypeParametersCST() &lt;SLASH&gt;
     *       | ModulePathCST() [ ModuleNameCST() TypeParametersCST() &lt;SLASH&gt; ]
     * </PRE>
     * @param packageNameCST_, package Name node of the CST
     * @param argu_ not used
     * @return AST {@link Path}
     */
    public Object visit(PackageNameCST packageNameCST_, Object argu_) {
	Ids ids = null;
	Location location = null;
	
	NodeSequence nodes = (NodeSequence) packageNameCST_.nodeChoice.choice;
		if (packageNameCST_.nodeChoice.which == 0) {
			// ModuleNameCST() TypeParametersCST() &lt;SLASH&gt;
			Id moduleId = (Id) nodes.elementAt(0).accept(this, nodes.elementAt(1).accept(this, argu_));
			ids = new Ids();
			ids.addId(moduleId);
			location = new Location(moduleId, (NodeToken) nodes.elementAt(2));
		} else {
			// ModulePathCST() [ ModuleNameCST() TypeParametersCST()
			// &lt;SLASH&gt; ]
			Path modulePath = (Path) nodes.elementAt(0).accept(this, argu_);

			ids = modulePath.getPackages();

			if (!((NodeOptional) nodes.elementAt(1)).present()) {
				// since the optional node is not present,
				// the last Id in the ModulePathCST() should actually be a
				// ModuleId

				Id lastId = (Id) ids.childAt(ids.numChildren() - 1);
				ModuleId moduleId = new ModuleId(lastId.getLocation(), lastId.nodeString(), new QualifiedNames());
				ids.setChild(ids.numChildren() - 1, moduleId);

				location = modulePath.getLocation();
			} else {
				NodeSequence optional = (NodeSequence) ((NodeOptional) nodes.elementAt(1)).node;

				Id moduleId = (Id) optional.elementAt(0).accept(this, optional.elementAt(1).accept(this, argu_));
				ids.addId(moduleId);

				location = new Location(modulePath, (NodeToken) optional.elementAt(2));
			}

		}

	return new Path(location,ids);

    }

    /**
     * <PRE>
     * nodeToken -> &lt;ID&gt;
     * nodeToken1 -> &lt;SLASH&gt;
     * </PRE>
     * @param dirCST_, the DirCST node
     * @param argu_, not used
     * @return AST {@link ID}
     */
    public Object visit(DirCST dirCST_, Object argu_) {
        Location location = new Location(_fileName, dirCST_.nodeToken);
        return new Id(location, dirCST_.nodeToken.tokenImage);
    }

    /**
     * <PRE>
     * nodeToken -> &lt;ID&gt;
     * </PRE>
     * @param aliasCST_, the AliasCST node
     * @param argu_, not used
     * @return AST {@link QualifiedName}
     */
    public Object visit(AliasCST aliasCST_, Object argu_) {
        // note that the id of the alias must be a ModuleId,
	// since the alias is treated as a module name

        Location location = new Location(_fileName, aliasCST_.nodeToken);
        QualifiedNames qualifiedNames = new QualifiedNames();

        QualifiedName alias = 
            new QualifiedName(
                new Location(_fileName, aliasCST_.nodeToken),
                new ModuleId(
                    new Location(_fileName, aliasCST_.nodeToken),
                    aliasCST_.nodeToken.tokenImage, new QualifiedNames()),
                new Path());

        return alias;
    }

    /**
     * <PRE>
     * nodeChoice -> PackageNameCST() &lt;ID&gt;
     *       | &lt;ID&gt;
     *       | &lt;SIGINT&gt;
     * </PRE>
     * @param sigNameCST_, Signature Name node of the CST
     * @param argu_ not used
     * @return AST {@link QualifiedName}
     */
    public Object visit(SigNameCST sigNameCST_, Object argu_) {
        alloy.parse.syntaxtree.Node choice = sigNameCST_.nodeChoice.choice;
        QualifiedName retName = null;
        // switch on production
        switch (sigNameCST_.nodeChoice.which) {
            case 0 : // PackageNameCST <ID>
                NodeSequence sigSeq = (NodeSequence) choice;
                /***********GET PATH*********************************************/
                Path path = (Path) sigSeq.elementAt(0).accept(this, null);

                /***********GET ID***********************************************/
                NodeToken sigToken = (NodeToken) sigSeq.elementAt(1);
                Location tokenLocation = new Location(_fileName, sigToken);
                Id id = new Id(tokenLocation, sigToken.tokenImage);

                /***********GET LOCATION*****************************************/
                Location location = new Location(path, id);

                retName = new QualifiedName(location, id, path);

                /*
                // module importing scheme: aliases are transparent
                println(debugSwitch, "_aliasesToModuleNames = " + _aliasesToModuleNames);
                println(debugSwitch, "retName = " + retName);
                */
                break;
            case 1 : // <ID>
                NodeToken sToken = (NodeToken) choice;
                Location sIdLocation = new Location(_fileName, sToken);
                Id sId = new Id(sIdLocation, sToken.tokenImage);
                //println(debugSwitch, "SigNameCST: " + sToken);
                //println(debugSwitch, "SigNameCST: " + _environ);
                // handler for polymorphism
                // if(!_environ.isTopLevel() && _environ.hasBinding(sToken.tokenImage)) {
                QualifiedName sig = new QualifiedName(sId, _curPath);
                if(!_environ.isTopLevel() && _environ.hasBinding(sig)) {
                    //println(debugSwitch, "Binding " + sToken.tokenImage + "@" + _curPath);

/*
                    TypeElementAndPath pair = _environ.getBinding(sId, _curPath);
                    
                    Path varPath = pair.getPath();
                    Id varId = pair.getTypeElement();
*/
					retName = _environ.getBinding(sig);
                    // use the location of the actual sig
                    Location loc = new Location(sToken, sId);
                    retName.setLocation(loc);
                    //retName = new QualifiedName(loc, varId, varPath);

                } else {
                    retName =
                        new QualifiedName(sIdLocation, sId, new Path());
                }

                break;
            case 2 : // <SIGINT>
                NodeToken intToken = (NodeToken) choice;
                Id intId =
                    new Id(
                        new Location(_fileName, intToken),
                        intToken.tokenImage);
                retName =
                    new QualifiedName(intId.getLocation(), intId, new Path());
                break;
        }

        return retName;
    }

    /**
     * <PRE>
     * nodeOptional -> [ PackageNameCST() &lt;SLASH&gt; ]
     * nodeToken -> &lt;ID&gt;
     * </PRE>
     *
     * @param paraNameCST_, Paragraph Name node of the CST
     * @param argu_ not used
     * @return AST {@link QualifiedName}
     */
    public Object visit(ParaNameCST paraNameCST_, Object argu_) {

        /***********GET PATH*********************************************/
        Path path = new Path();
        if (paraNameCST_.nodeOptional.present()) {
            //paraNameCST_.nodeOptional is of type PackageNameCST
            //println(debugSwitch, "Class: " + paraNameCST_.nodeOptional.node.getClass());
            path = (Path)paraNameCST_.nodeOptional.node.accept(this, null);

            // converts aliases to real paths, if necessary
            //path = translateToRealPath(path);
        }

        /***********GET ID***********************************************/
        Location tokenLocation =
            new Location(_fileName, paraNameCST_.nodeToken);
        Id id = new Id(tokenLocation, paraNameCST_.nodeToken.tokenImage);

        /***********GET LOCATION*****************************************/
        Location location = id.getLocation();

        return new QualifiedName(location, id, path);
    }

    /**
     * <PRE>
     * nodeChoice -> PackageNameCST() &lt;ID&gt;
     *       | &lt;ID&gt;

     * nodeOptional -> [ PackageNameCST() ]
     * nodeChoice -> ( &lt;ID&gt; | &lt;UNIV&gt; | &lt;SIGINT&gt; )


     * </PRE>
     * @param typeArgCST_, Type Argument node of the CST
     * @param argu_ the environment of the imported module
     * @return AST {@link QualifiedName}
     */
    public Object visit(TypeArgCST typeArgCST_, Object argu_) {
    	
    	Node choice = typeArgCST_.nodeChoice.choice;
    	
    	// Get the token, it could be <ID>, <UNIV>, or <SIGINT>
    	NodeToken typeArgToken = (NodeToken) choice;
    	String id = typeArgToken.tokenImage;
    	
    	Location typeArgLocation = new Location(_fileName, typeArgToken);
    	Id typeArg = new Id(typeArgLocation, id);
    	
    	// if the token is <SIGINT>, then we should lazily import 
    	// the Int module
    	if (typeArgCST_.nodeChoice.which == 2) { // <SIGINT>
    		_importInt();
    	} 
    	
    	QualifiedName retName = null;
    	
    	if (typeArgCST_.nodeOptional.present()) {
    		Path typeArgPath = 
    			(Path) typeArgCST_.nodeOptional.node.accept(this,null);
    		
    		// check if path has one ID and is an alias, if so replace with module name
    		// otherwise the alias will propagate to the imported module
    		Ids pathIds = typeArgPath.getPackages();
    		int pathSize = pathIds.numChildren();
    		
    		if(pathSize == 1) {
    			QualifiedName aliasName = new QualifiedName((Id) pathIds.getIdIter().next(), new Path());
    			QualifiedName parentName = (QualifiedName) _aliasesToModuleNames.get(aliasName);
    			
    			Ids moduleNameIds = new Ids();
    			
    			if (parentName == null) { // this is not an alias
    				parentName = aliasName;
    			}
    			
    			for (Iterator i = parentName.getPath().getPackages().getIdIter(); i.hasNext();) {
    				moduleNameIds.addId((Id)i.next()); }
    			
    			moduleNameIds.addId(parentName.getId());
    			typeArgPath = new Path(typeArgPath.getLocation(), moduleNameIds);
    		} 
    		retName = new QualifiedName(new Location(typeArgPath,typeArg), typeArg, typeArgPath);
    	} else {
    		
    		// check that the type argument is sig found in prepass, or univ, or Int
    		if(!_signatureNames.contains(typeArgToken.tokenImage) && 
    				!typeArgToken.tokenImage.equals(UNIV) && 
					!typeArgToken.tokenImage.equals(INT)) {
    			println(_debugSwitch, "Current Module: " + _currentModuleName);
    			Dbg.user(new Msg("Reference to unknown signature " + typeArg, typeArg));
    		}
    		
    		if  (typeArgCST_.nodeChoice.which == 0) {// <ID>
    			retName =  new QualifiedName(typeArgLocation, typeArg, (Path) _curPath.copy());
    		} else { // <UNIV> or <SIGINT>
    			retName = new QualifiedName(typeArgLocation, typeArg, 
    					_getLangModuleName(typeArgCST_.nodeChoice.which==1 ? 
    							UNIV : INT));	    
    		}
    	}
    	
    	((Environment)argu_).addArgToBind(retName);
    	return retName;
    }

    /**
     * <PRE>
     * nodeToken -> &lt;ID&gt;
     * </PRE>
     * @param typeVarCST_, Type Variable node of the CST
     * @param argu_ not used
     * @return AST {@link Id}
     */
    public Object visit(TypeVarCST typeVarCST_, Object argu_) {

        /***********GET ID***********************************************/
        String id = typeVarCST_.nodeToken.tokenImage;

        /***********GET LOCATION*****************************************/
        Location location = new Location(_fileName, typeVarCST_.nodeToken);

        return new Id(location, id);
    }

    /**
     * <PRE>
     * nodeChoice -> PackageNameCST() &lt;ID&gt;
     *       | &lt;ID&gt;
     
     * nodeOptional -> [ PackageNameCST() ]
     * nodeChoice -> ( &lt;ID&gt; | &lt;UNIV&gt; | &lt;SIGINT&gt; )


     * </PRE>
     * @param typeParameterCST_, Type Parameter node of the CST
     * @param argu_ not used
     * @return AST {@link QualifiedName}
     */
    public Object visit(TypeParameterCST typeParameterCST_, Object argu_) {
	
	Node choice = typeParameterCST_.nodeChoice.choice;

	// Get the token, it could be <ID>, <UNIV>, or <SIGINT>
	NodeToken typeParamToken = (NodeToken) choice;
	String id = typeParamToken.tokenImage;

	Location typeParamLocation = new Location(_fileName, typeParamToken);
	Id typeParam = new Id(typeParamLocation, id);

	// if the token is <SIGINT>, then we should lazily import 
	// the Int module
	if (typeParameterCST_.nodeChoice.which == 2) { // <SIGINT>
	    _importInt();
	} 

	if (typeParameterCST_.nodeOptional.present()) {
	    Path typeParamPath = 
		(Path) typeParameterCST_.nodeOptional.node.accept(this,null);
	    return new QualifiedName(new Location(typeParamPath,typeParam),
				     typeParam, typeParamPath);
	} else {
	    
	    if  (typeParameterCST_.nodeChoice.which == 0) {// <ID>
		return new QualifiedName(typeParamLocation, typeParam, (Path) _curPath.copy());
	    } else { // <UNIV> or <SIGINT>
		return new QualifiedName(typeParamLocation, typeParam, 
					 _getLangModuleName(typeParameterCST_.nodeChoice.which==1 ? 
							    UNIV : INT));	    
	    }
	}



	/**
        Node choice = typeParameterCST_.nodeChoice.choice;

        if(typeParameterCST_.nodeChoice.which == 0) {
            // PackageNameCST() <ID>
            NodeSequence typeParamSeq = (NodeSequence) choice;
	    // GET PATH
            Path typeParamPath = (Path) typeParamSeq.elementAt(0).accept(this, null);

            // GET ID
            NodeToken typeArgToken = (NodeToken) typeParamSeq.elementAt(1);
            String id = typeArgToken.tokenImage;

            Location typeParamLocation = new Location(_fileName, typeArgToken);
            Id typeParam = new Id(typeParamLocation, id);

            return new QualifiedName(new Location(typeParamPath,typeParam),
				     typeParam, typeParamPath);

        } else {
            // <ID>
            // GET PATH
            Path typeParamPath = _curPath;

            // doesn't use package name

	    // GET ID
            NodeToken typeParamToken = (NodeToken) choice;
            String id = typeParamToken.tokenImage;

            Location typeParamLocation = new Location(_fileName, typeParamToken);
            Id typeParam = new Id(typeParamLocation, id);

            return new QualifiedName(typeParamLocation, typeParam,
				     (Path) typeParamPath.copy());

        }
    **/
    }

    /****************************************************************
     *                    DECLARATION STUFF                         *
     *                                                              *
     * DeclCST       => Decl                                        *
     * CompOpCST     => CompOp                                      *
     * MultExprCST   => MultiplicityExpr                            *
     * QualifierCST  => Qualifier                                   *
     * QuantifierCST => Quantifier                                  *
     * VarCST        => Variable                                    *
     * MultCST       => Multiplicity                                *
     ****************************************************************/

    /**
     * <PRE>
     * nodeListOptional -> ( QualifierCST() )*
     * varCST -> VarCST()
     * nodeListOptional1 -> ( &lt;COMMA&gt; VarCST() )*
     * nodeToken -> &lt;COLON&gt;
     * multExprCST -> MultExprCST()
     * </PRE>
     * @param declCST_ Decl node of the CST
     * @param argu_ not used
     * @return AST {@link Decl}
     */
    public Object visit(DeclCST declCST_, Object argu_) {

    Qualifiers qualifiers = new Qualifiers();

    // qualifiers specified
        if (declCST_.nodeListOptional.present()) {
            /***********GET QUALIFIERS******************************************/
            Enumeration qualCSTNodes = declCST_.nodeListOptional.elements();
            // add the first qualifier
            Qualifier firstQual =
                (Qualifier) ((QualifierCST) qualCSTNodes.nextElement()).accept(
                    this,
                    null);
            qualifiers.addQualifier(firstQual);
        Set declaredQuals = new HashSet();
        declaredQuals.add(firstQual);

        Qualifier currentQual = firstQual;
            while (qualCSTNodes.hasMoreElements()) {
                currentQual =
                    (Qualifier)
                        ((QualifierCST) qualCSTNodes.nextElement()).accept(
                        this,
                        null);
                qualifiers.addQualifier(currentQual);
        if (!declaredQuals.add(currentQual)) {
            error(currentQual.nodeString() + " already specified", currentQual);
        }
            }
            qualifiers.setLocation(new Location(firstQual, currentQual));
        }

        /***********GET VARIABLES******************************************/
        Variables variables = new Variables();
        //add first variable
        Variable firstVariable = (Variable) declCST_.varCST.accept(this, null);
        variables.addVariable(firstVariable);
        Variable currentVariable;

        Enumeration vars = declCST_.nodeListOptional1.elements();
        while (vars.hasMoreElements()) {
            currentVariable =
                (Variable)
        ((VarCST) ((NodeSequence) vars.nextElement()).
         elementAt(1)).accept(this,null);
            variables.addVariable(currentVariable);
        }

        variables.setLocation(firstVariable.getLocation());


        /***********GET MULTEXPRESSION************************************/
        MultiplicityExpr multiplicityExpr =
            (MultiplicityExpr) declCST_.multExprCST.accept(this,null);

        /***********GET LOCATION*****************************************/
        Location location;
        //if second choice
        if (declCST_.nodeListOptional.present()) {
            location = new Location(qualifiers, multiplicityExpr);
        } else {
            location = new Location(variables, multiplicityExpr);
        }

        return new Decl(
            location,
            qualifiers,
            variables,
            multiplicityExpr);

    }

    /**
     * <PRE>
     * nodeOptional -> [ NegOpCST() ]
     * nodeChoice -> ( &lt;COLON&gt; | &lt;EQUALS&gt; | &lt;IN&gt; )
     * </PRE>
     * @param compOpCST_ the Comp. Op. CST node
     * @param argu_ not used
     * @return AST {@link CompOp}
     */
    public Object visit(CompOpCST compOpCST_, Object argu_) {
        CompOp op = null;
        switch(compOpCST_.nodeChoice.which) {
        	case 0: op = CompOp.SUBSETCOLON; break;
        	case 1: op = CompOp.EQUALS; break;
        	case 2: op = CompOp.SUBSETIN; break;
        	default: Dbg.chk(false);
        }
        
        return compOpCST_.nodeOptional.present() ? op.negation() : op;
    }

    /**
     * @param expr Expr
     * @return MultiplicityExpr that corresponds to expr.  Note that if expr
     * has the form e1->e2, then it is recursively converted to ArrowMultExpr, 
     * so that if e2 = e3->e4, we return an ArrowMultExpr whose left expression 
     * is a SetMultExpr e1 and whose right expression is an ArrowMultExpr e3->e4
     **/
    private static MultiplicityExpr convertToMultExpr(Expr expr) {
		MultiplicityExpr multExpr = null;
		if (expr instanceof BinaryExpr) {
		    BinaryExpr binExpr = (BinaryExpr) expr;
		    if (binExpr.getOp().equals(BinaryExprOp.RELATION)) {
		        multExpr =  new ArrowMultExpr(Multiplicity.NONE,
						      convertToMultExpr(binExpr.getLeft()),
						      convertToMultExpr(binExpr.getRight()));
		    }
		}

		if (multExpr == null) multExpr =  new SetMultExpr(Multiplicity.NONE, expr);
		multExpr.setLocation(expr.getLocation());
		return multExpr;
    }

   /**
    * <PRE>
    * nodeChoice -> ( ExprCST() | &lt;LPAREN&gt; RelMultExprCST() &lt;RPAREN&gt; )
    * nodeOptional -> [ [ MultCST() ] &lt;ARROW&gt; [ MultCST() ] RelMultExprCST() ]
    * </PRE>
    * @param relMultExprCST_ the Rel. Mult. Expr. CST node
    * @param argu_ not used
    * @return AST {@link MultiplicityExpr}
    */
    public Object visit(RelMultExprCST relMultExprCST_, Object argu_) {

	MultiplicityExpr leftExpr;

	
	if (relMultExprCST_.nodeChoice.which == 0) { // ExprCST() 
	    Expr expr = (Expr) relMultExprCST_.nodeChoice.choice.accept(this,null);
	    // if expr has the form e1->e2, then left expr is an arrow mult expr,
	    // otherwise, it's a set mult expr
	    leftExpr = convertToMultExpr(expr);
	
	} else {  // &lt;LPAREN&gt; RelMultExprCST() &lt;RPAREN&gt; 
	    NodeSequence nodes = ((NodeSequence) relMultExprCST_.nodeChoice.choice);
	    //leftExpr = 
	    //	(MultiplicityExpr) 
	    //	((NodeSequence) relMultExprCST_.nodeChoice.choice).elementAt(1).accept(this,null);
	    leftExpr = (MultiplicityExpr)nodes.elementAt(1).accept(this, null);
	    
	    ((TreeNode)leftExpr).setLocation(new Location(leftExpr.getLocation().getFileName(), 
							 (NodeToken)nodes.elementAt(0), 
							 (NodeToken)nodes.elementAt(2)));
	}

	// ( ExprCST() | &lt;LPAREN&gt; RelMultExprCST() &lt;RPAREN&gt; ) 
	// [ MultCST() ] &lt;ARROW&gt; [ MultCST() ] RelMultExprCST() 
	if (relMultExprCST_.nodeOptional.present()) {
	    NodeSequence nodes = (NodeSequence) relMultExprCST_.nodeOptional.node;

	    int nodesLength = nodes.size();
	    
	    MultiplicityExpr rightExpr = 
		(MultiplicityExpr) nodes.elementAt(nodesLength - 1).accept(this,null);
	    
	    NodeOptional leftMultCST = (NodeOptional) nodes.elementAt(0);
	    
	    if (leftMultCST.present()) {
		Multiplicity leftMult = (Multiplicity) leftMultCST.node.accept(this,null);
		leftExpr.setMult(leftMult);
		leftExpr.setLocation(new Location(leftExpr, leftMult));
	    }
	    
	    NodeOptional rightMultCST = (NodeOptional) nodes.elementAt(nodesLength - 2);

	    if (rightMultCST.present()) {
		Multiplicity rightMult = (Multiplicity) rightMultCST.node.accept(this,null);
		rightExpr.setMult(rightMult);
		rightExpr.setLocation(new Location(rightMult, rightExpr));
	    }

	    return new ArrowMultExpr(new Location(leftExpr, rightExpr),
				     Multiplicity.NONE, leftExpr, rightExpr);

	} else {
	    return leftExpr;
	}
    }
    
    /**
     * <PRE>
     * nodeOptional -> [ MultCST() ]
     * relMultExprCST -> RelMultExprCST()
     * </PRE>
     * @param multExprCST_ the Mult. Expr. CST node
     * @param argu_ not used
     * @return AST {@link MultiplicityExpr}
     */
    public Object visit(MultExprCST multExprCST_, Object argu_) {
	
	
	MultiplicityExpr multExpr = 
	    (MultiplicityExpr) multExprCST_.relMultExprCST.accept(this,null); 
	
	
	if (multExprCST_.nodeOptional.present()) {
	    Multiplicity mult = 
		(Multiplicity) multExprCST_.nodeOptional.node.accept(this,null);
	    multExpr.setMult(mult);
	    multExpr.setLocation(new Location(mult, multExpr));
	} 

	return multExpr;
    }

    /**
     * <PRE>
     * nodeChoice -> &lt;PART&gt; | &lt;DISJ&gt;  | &lt;EXH&gt;
     * </PRE>
     * @param qualifierCST_ the Qualifier CST node
     * @param argu_ not used
     * @return AST {@link Qualifier}
     */
    public Object visit(QualifierCST qualifierCST_, Object argu_) {
        switch(qualifierCST_.nodeChoice.which) {
        	case 0: case 3: return Qualifier.PART;
        	case 1: case 4: return Qualifier.DISJ;
        	case 2: case 5: return Qualifier.EXH;
        	default: Dbg.chk(false); return null;
        }
    }

    /**
     * <PRE>
     * nodeChoice -> &lt;ALL&gt; | &lt;NO&gt; | &lt;SOME&gt; | &lt;LONE&gt; | &lt;ONE&gt;
     * </PRE>
     * @param quantifierCST_ the Quantifier CST node
     * @param argu_ not used
     * @return AST {@link Quantifier}
     */
    public Object visit(QuantifierCST quantifierCST_, Object argu_) {
        switch(quantifierCST_.nodeChoice.which) {
        	case 0: return Quantifier.ALL;
        	case 1: return Quantifier.NO;
        	case 2: return Quantifier.SOME;
        	case 3: return Quantifier.LONE;
        	case 4: return Quantifier.ONE;
        	default: Dbg.chk(false); return null;
        }
    }

    /**
     * <PRE>
     * nodeOptional -> [ &lt;AT&gt; ]
     * nodeToken -> &lt;ID&gt;
     * </PRE>
     * @param varCST_ the Var CST node
     * @param argu_ not used
     * @return AST {@link Variable}
     */
    public Object visit(VarCST varCST_, Object argu_) {

        /***********GET NAME*****************************************/
        Location location = new Location(_fileName, varCST_.nodeToken);
        Id name = new Id(location, varCST_.nodeToken.toString());

        /***********CHECK FOR VARIABLE SHADOWING*********************/
        noShadow(name);

        boolean flagged = varCST_.nodeOptional.present();
        return new Variable(location, name, flagged);
    }


    /**
    * <PRE>
    * nodeChoice -> &lt;LONE&gt; | &lt;ONE&gt; | &lt;SOME&gt; | &lt;SET&gt;
    * </PRE>
    * @param multCST_ the Mult CST node
    * @param argu_ not used
    * @return AST {@link Multiplicity}
    */
    public Object visit(MultCST multCST_, Object argu_) {
        switch(multCST_.nodeChoice.which) {
        	case 0: return Multiplicity.LONE;
        	case 1: return Multiplicity.ONE;
        	case 2: return Multiplicity.SOME;
        	case 3: return Multiplicity.SET;
        	default: Dbg.fail("no such multiplicity"); return null;
        }
    }

    /**
     * <PRE>
     * varCST -> VarCST()
     * nodeToken -> &lt;EQUALS&gt;
     * exprCST -> ExprCST()
     * </PRE>
     * @return AST {@link LetDecl}
     */
    public Object visit(LetDeclCST letDeclCST_, Object argu_) {
        Variable var = (Variable) letDeclCST_.varCST.accept(this, null);
        Expr expr = (Expr) letDeclCST_.exprCST.accept(this, null);
        Location loc = new Location(var, expr);
        return new LetDecl(loc, var, expr);
    }

    /****************************************************************
     *                    EXPRESSION STUFF                          *
     *                                                              *
     * all convert to type Expr                                     *
     * ExprCST                                                      *
     * WithOrLetExprCST                                                  *
     * UnionDiffExprCST                                             *
     * IntersectExprCST                                             *
     * RelationExprCST                                              *
     * BracketExprCST                                               *
     * DotExprCST                                                   *
     * UnopExprCST                                                  *
     * DoubleColonExprCST                                           *
     * OtherExprCST                                                 *
     *                                                              *
     * InvocationBaseCST => InvocationExpr                          *
     * SigCST => SigExpr                                            *
     * ParamSigName => SigExpr                                      *
     * UnionDiffOpCST => BinaryExprOp                               *
     * UnOpCST => UnaryExprOp                                       *
     ****************************************************************/

    /**
     * <PRE>
     * nodeChoice -> WithOrLetExprCST()
     *       | UnionDiffExprCST()
     * @param exprCST_ the Expr CST node
     * @param argu_ not used
     * @return AST {@link Expr}
     */
    public Object visit(ExprCST exprCST_, Object argu_) {
        // we just want to visit the child and return the result,
        // for either choice
        return exprCST_.nodeChoice.choice.accept(this, null);
    }

    /**
     * <PRE>
     * nodeToken -> &lt;LET&gt;
     * letDeclCST -> LetDeclCST()
     * nodeListOptional -> ( &lt;COMMA&gt; LetDeclCST() )*
     * nodeToken1 -> &lt;BAR&gt;
     * exprCST -> ExprCST()
     * @param withOrLetExprCST_ the With Expr CST node
     * @param argu_ not used
     * @return AST {@link Expr}
     */
    public Object visit(LetExprCST letExprCST_, Object argu_) {
        Expr ret = null;
        Location location;
        // get <LET> token for location
        NodeToken letToken = (NodeToken) letExprCST_.nodeToken;
        // get let decls
        LetDecls letDecls = new LetDecls();
        letDecls.addLetDecl(
            (LetDecl) letExprCST_.letDeclCST.accept(this, null));
        for (Enumeration enum2 = letExprCST_.nodeListOptional.elements();
            enum2.hasMoreElements();
            ) {
            // get rid of comma:  enum.nextElement is the sequence
	    // (&lt;COMMA&gt; LetDeclCST())
	    letDecls.addLetDecl(
                (LetDecl) 
		(((NodeSequence) enum2.nextElement()).elementAt(1)).
		accept(this, null));
        }

        Expr body = (Expr) letExprCST_.exprCST.accept(this, null);

        location = new Location(letToken, body);
        ret = new LetExpr(location, letDecls, body);
        return ret;
    }

    /**
     * <PRE>
     * relationalOverrideExprCST -> RelationalOverrideExprCST()
     * nodeOptional -> [ ( UnionDiffOpCST() UnionDiffExprCST() | UnionDiffOpCST() WithOrLetExprCST() ) ]
     * </PRE>
     * @param unionDiffExprCST_ the Union. Diff. CST node
     * @param argu_ not used
     * @return AST {@link Expr}
     */
    public Object visit(UnionDiffExprCST unionDiffExprCST_, Object argu_) {
        /***********GET LEFT EXPR*****************************************/
        Expr leftExpr =
            (Expr) unionDiffExprCST_.relationalOverrideExprCST.accept(
                this,
                null);
        Expr retExpr = leftExpr;
        // see if this actually has a right expr
        if (unionDiffExprCST_.nodeOptional.present()) {
            NodeChoice nChoice =
                (NodeChoice) unionDiffExprCST_.nodeOptional.node;
            NodeSequence unionDiffExprNodes = (NodeSequence) nChoice.choice;
            /***********GET OPERATOR*****************************************/
            BinaryExprOp op =
                (BinaryExprOp) unionDiffExprNodes.elementAt(0).accept(
                    this,
                    null);
            /***********GET RIGHT EXPR*****************************************/
            Expr rightExpr =
                (Expr) unionDiffExprNodes.elementAt(1).accept(this, null);
            /***********GET LOCATION*****************************************/
            Location location = new Location(leftExpr, rightExpr);
            retExpr = new BinaryExpr(location, leftExpr, op, rightExpr);
            // if necessary, transform expression to make it left associative
            retExpr = _makeLeftAssociative((BinaryExpr) retExpr);
        }
        return retExpr;
    }

    /**
     * Make a binary expression left-associative.
     * @param binExpr_ binary expression to be transformed.  Assumes RHS
     * of <code>binExpr_</code> has already been transformed
     */
    private BinaryExpr _makeLeftAssociative(BinaryExpr binExpr_) {
        BinaryExpr retExpr = binExpr_;
        Expr left = binExpr_.getLeft();
        Expr right = binExpr_.getRight();

        // if (right.hasParens()) System.out.println(right);

        BinaryExprOp op = binExpr_.getOp();
        // see if transformation is applicable
        if ((right instanceof BinaryExpr) // RHS must be binary expr
            && !right.hasParens() // RHS must not be parenthesized
            && _opsMatch(right, op)) { // RHS must have same operator
            // tranform e1 op (e2 op e3) to (e1 op e2) op e3,
            // maintaing proper location information
            BinaryExprOp rightOp = ((BinaryExpr) right).getOp();
            Expr mid = ((BinaryExpr) right).getLeft();
            Expr farRight = ((BinaryExpr) right).getRight();
            Expr tmpExpr =
                new BinaryExpr(new Location(left, mid), left, op, mid);
            // ensure new LHS is left associative
            tmpExpr = _makeLeftAssociative((BinaryExpr) tmpExpr);
            retExpr =
                new BinaryExpr(
                    new Location(tmpExpr, farRight),
                    tmpExpr,
                    rightOp,
                    farRight);
        }
        return retExpr;
    }

    private boolean _opsMatch(Expr right, BinaryExprOp leftOp) {
       BinaryExprOp rightOp = ((BinaryExpr) right).getOp();
        return (leftOp.equals(rightOp) && !leftOp.equals(BinaryExprOp.JOIN_SQBRACKETS))
            || (leftOp.equals(BinaryExprOp.UNION) && rightOp.equals(BinaryExprOp.DIFF))
            || (leftOp.equals(BinaryExprOp.DIFF) && rightOp.equals(BinaryExprOp.UNION))
            || (leftOp.equals(BinaryExprOp.JOIN_DOT) && rightOp.equals(BinaryExprOp.JOIN_SQBRACKETS));
    }

    /**
     * <PRE>
     * intersectExprCST -> IntersectExprCST()
     * nodeOptional -> [ ( &lt;PLUSPLUS&gt; RelationalOverrideExprCST() | &lt;PLUSPLUS&gt; WithOrLetExprCST() ) ]
     * </PRE>
     * @param relationalOverideExprCST_ the relationalOverideExpr CST node
     * @param argu_ not used
     * @return AST {@link Expr}
     */
    public Object visit(
        RelationalOverrideExprCST relationalOverrideExprCST_,
        Object argu) {
        /***********GET LEFT EXPR*****************************************/
        Expr leftExpr =
            (Expr) relationalOverrideExprCST_.intersectExprCST.accept(
                this,
                null);
        Expr retExpr = leftExpr;
        // see if this actually has a right expr
        if (relationalOverrideExprCST_.nodeOptional.present()) {
            NodeChoice nChoice =
                (NodeChoice) relationalOverrideExprCST_.nodeOptional.node;
            NodeSequence exprNodes = (NodeSequence) nChoice.choice;
            /***********GET RIGHT EXPR*****************************************/
            Expr rightExpr = (Expr) exprNodes.elementAt(1).accept(this, null);
            /***********GET LOCATION*****************************************/
            Location location = new Location(leftExpr, rightExpr);
            retExpr = new BinaryExpr(location, leftExpr, BinaryExprOp.RELATIONALOVERRIDE, rightExpr);
        }
        return retExpr;
    }

    /**
     * <PRE>
     * relationExprCST -> RelationExprCST()
     * nodeOptional -> [ ( &lt;AMPERSAND&gt; IntersectExprCST() | &lt;AMPERSAND&gt; WithOrLetExprCST() ) ]
     * </PRE>
     * @param intersectExprCST_ the InsersectExpr CST node
     * @param argu_ not used
     * @return AST {@link Expr}
     */
    public Object visit(IntersectExprCST intersectExprCST_, Object argu_) {
        /***********GET LEFT EXPR*****************************************/
        Expr leftExpr =
            (Expr) intersectExprCST_.relationExprCST.accept(this, null);
        Expr retExpr = leftExpr;
        // see if this actually has a right expr
        if (intersectExprCST_.nodeOptional.present()) {
            NodeChoice nChoice =
                (NodeChoice) intersectExprCST_.nodeOptional.node;
            NodeSequence exprNodes = (NodeSequence) nChoice.choice;
            /***********GET RIGHT EXPR*****************************************/
            Expr rightExpr = (Expr) exprNodes.elementAt(1).accept(this, null);
            /***********GET LOCATION*****************************************/
            Location location = new Location(leftExpr, rightExpr);
            retExpr = new BinaryExpr(location, leftExpr, BinaryExprOp.INTERSECT, rightExpr);
        }
        return retExpr;
    }

    /**
     * <PRE>
     * invocationExprCST -> InvocationExprCST()
     * nodeOptional -> [ ( &lt;ARROW&gt; RelationExprCST() | &lt;ARROW&gt; WithOrLetExprCST() ) ]
     * </PRE>
     * @param relationExprCST_ the relation Expr CST node
     * @param argu_ not used
     * @return AST {@link Expr}
     */
    public Object visit(RelationExprCST relationExprCST_, Object argu_) {
        /***********GET LEFT EXPR*****************************************/
        Expr leftExpr =
            (Expr) relationExprCST_.invocationExprCST.accept(this, null);
        Expr retExpr = leftExpr;
        // see if this actually has a right expr
        if (relationExprCST_.nodeOptional.present()) {
            NodeChoice nChoice =
                (NodeChoice) relationExprCST_.nodeOptional.node;
            NodeSequence exprNodes = (NodeSequence) nChoice.choice;
            /***********GET RIGHT EXPR*****************************************/
            Expr rightExpr = (Expr) exprNodes.elementAt(1).accept(this, null);
            /***********GET LOCATION*****************************************/
            Location location = new Location(leftExpr, rightExpr);
            retExpr = new BinaryExpr(location, leftExpr, BinaryExprOp.RELATION, rightExpr);
        }
        return retExpr;
    }

    /**
     * <PRE>
     * bracketOrDotExprCST -> BracketOrDotExprCST()
     * nodeListOptional -> ( &lt;DOUBLEDOT&gt; InvocationBaseCST() )*
     * nodeOptional -> [ &lt;DOT&gt; InvocationExprCST() ]
     * </PRE>
     * @param invocationExprCST_ the InvocationExprCST node
     * @param argu_ not used
     * @return AST {@link Expr}
     */
    public Object visit(InvocationExprCST invocationExprCST_, Object argu_) {
        /***********GET LEFT EXPR*****************************************/
        Expr leftExpr =
            (Expr) invocationExprCST_.domainExprCST.accept(this, null);
        InvocationExpr rightExpr;
        Expr retExpr = leftExpr;
        Location location;

        // check if we really have an invocation
        if (invocationExprCST_.nodeListOptional.present()) {

            // loop to get all the invocation expressions
            Enumeration invocationExprs =
                invocationExprCST_.nodeListOptional.elements();
            while (invocationExprs.hasMoreElements()) {

                /***********GET RIGHT EXPR*****************************************/
                rightExpr =
                    (InvocationExpr)
                        (
                            (InvocationBaseCST)
                                (
                                    (NodeSequence) invocationExprs
                                        .nextElement())
                                        .elementAt(
                                1)).accept(
                        this,
                        null);

                /***********GET LOCATION***********************************************/
                location = new Location(retExpr, rightExpr);

                retExpr =
                    new InvocationExpr(
                        location,
                        retExpr,
                        rightExpr.getInvocableName(),
                        rightExpr.getExprs());
            }
        }

        // check if invocation is followed by dot or doublecolon expr
        if (invocationExprCST_.nodeOptional.present()) {
            NodeSequence joinNodes =
                (NodeSequence) invocationExprCST_.nodeOptional.node;

            /***********GET OPERATOR*****************************************/
	    //System.out.println(joinNodes.elementAt(0) + " " + joinNodes.elementAt(0).getClass());
	    /** //Comment by Emina:  I'm not sure why the
		//code below was used for this production, 
                //given that joinNodes.elementAt(0) is <DOT> ?
            NodeChoice opChoice = (NodeChoice) joinNodes.elementAt(0);
            // the which trick works yet again
            int opCode = opChoice.which;
            NodeToken opToken = (NodeToken) opChoice.choice;
	    **/
	    NodeToken opToken = (NodeToken) joinNodes.elementAt(0);
            /***********GET RIGHT EXPR*****************************************/
            Expr endExpr =
                (Expr) ((InvocationExprCST) joinNodes.elementAt(1)).accept(
                    this,
                    null);

            /***********GET LOCATION***********************************************/
            location = new Location(retExpr, endExpr);
            retExpr = new BinaryExpr(location, retExpr, BinaryExprOp.JOIN_DOT, endExpr);
        }

        return retExpr;
    }

//    /**
//     * <PRE>
//     * dotExprCST -> DotExprCST()
//     * nodeListOptional -> ( &lt;LBRACKET&gt; ExprCST() &lt;RBRACKET&gt; )*
//     * nodeOptional -> [ ( &lt;DOT&gt; | &lt;DOUBLECOLON&gt; ) BracketExprCST() ]
//     * </PRE>
//     * @param bracketExprCST_ the InsersectExpr CST node
//     * @param argu_ not used
//     * @return AST {@link Expr}
//     */
//    public Object visit(BracketExprCST bracketExprCST_, Object argu_) {
//
//        /***********GET RIGHT EXPR*****************************************/
//        Expr rightExpr = (Expr) bracketExprCST_.dotExprCST.accept(this, null);
//        Expr leftExpr;
//        Expr retExpr = rightExpr;
//        Location location;
//
//        // check if we really have brackets
//        if (bracketExprCST_.nodeListOptional.present()) {
//
//            // loop to get all the bracketed expressions
//            Enumeration bracketedExprs =
//                bracketExprCST_.nodeListOptional.elements();
//            while (bracketedExprs.hasMoreElements()) {
//                NodeSequence curNodeSequence =
//                    ((NodeSequence) bracketedExprs.nextElement());
//
//                /***********GET LEFT EXPR*****************************************/
//                leftExpr =
//                    (Expr) ((ExprCST) curNodeSequence.elementAt(1)).accept(
//                        this,
//                        null);
//
//                // get right bracket
//                NodeToken rightBracket =
//                    (NodeToken) curNodeSequence.elementAt(2);
//
//                /***********GET LOCATION***********************************************/
//                location = new Location(retExpr, rightBracket);
//
//                retExpr =
//                    new BinaryExpr(
//                        location,
//                        leftExpr,
//                        new BinaryExprOp(
//                            Location.UNKNOWN,
//                            BinaryExprOp.JOIN_SQBRACKETS),
//                        retExpr);
//            }
//        }
//
//        // check if bracket expr is followed by dot or doublecolon expr
//        if (bracketExprCST_.nodeOptional.present()) {
//            NodeSequence joinNodes =
//                (NodeSequence) bracketExprCST_.nodeOptional.node;
//
//            /***********GET OPERATOR*****************************************/
//            NodeChoice opChoice = (NodeChoice) joinNodes.elementAt(0);
//            // the which trick works yet again
//            int opCode = opChoice.which;
//            NodeToken opToken = (NodeToken) opChoice.choice;
//            BinaryExprOp joinOp =
//                new BinaryExprOp(new Location(_fileName, opToken), opCode);
//
//            /***********GET RIGHT EXPR*****************************************/
//            rightExpr =
//                (Expr) ((BracketExprCST) joinNodes.elementAt(1)).accept(
//                    this,
//                    null);
//
//            /***********GET LOCATION***********************************************/
//            location = new Location(retExpr, rightExpr);
//            retExpr = new BinaryExpr(location, retExpr, joinOp, rightExpr);
//
//        }
//
//        return retExpr;
//    }
//

    // hideous; should really do this with arguments
    private boolean _bracketTopLevel = true;

    /**
     * <PRE>
     * domainExprCST -> DomainExprCST()
     * nodeOptional -> [ ( &lt;DOT&gt; LetExprCST() | ( ( &lt;LBRACKET&gt; ExprCST() &lt;RBRACKET&gt; | &lt;DOT&gt; BracketOrDotExprCST() ) )+ ) ]
     * </PRE>
     */
    public Object visit(BracketOrDotExprCST bracketExprCST_, Object argu) {
        Expr retExpr = null;
        // we'll do this in three steps
        // first, make AST nodes without flipping [] constructs
        // or fixing associativity
        boolean actualDotOrBracket = bracketExprCST_.nodeOptional.present();
        boolean myBracketTopLevel = false;
        if (actualDotOrBracket) {
            // we need to set and check this flag only when
            // we actually have a dot expression; otherwise,
            // an incorrect expression can be flagged as top-level
            myBracketTopLevel = _bracketTopLevel;
            _bracketTopLevel = false;
        }
        retExpr = (Expr)bracketExprCST_.unopExprCST.accept(this,null);
        if (actualDotOrBracket) {
            NodeChoice nodeChoice = (NodeChoice)bracketExprCST_.nodeOptional.node;
            switch (nodeChoice.which) {
                case 0: // <DOT> LetExprCST
                NodeSequence nodeSeq = (NodeSequence)nodeChoice.choice;
                NodeToken dotToken = (NodeToken) nodeSeq.elementAt(0);;
                Expr letExpr = (Expr)nodeSeq.elementAt(1).accept(this,null);
                retExpr = new BinaryExpr(new Location(retExpr,letExpr), retExpr, BinaryExprOp.JOIN_DOT,letExpr);
                break;
                case 1: // ([ ExprCST ] | <DOT> BracketOrDotExprCST)+
                NodeList nodeList = (NodeList)nodeChoice.choice;
                for (Enumeration enum2 = nodeList.elements(); enum2.hasMoreElements(); ) {
                    NodeChoice listElem = (NodeChoice)enum2.nextElement();
                    NodeSequence sequence = (NodeSequence)listElem.choice;
                    switch (listElem.which) {
                        case 0: // [ ExprCST ]
                        Expr innerExpr = (Expr)sequence.elementAt(1).accept(this,null);
                        retExpr = new BinaryExpr(new Location(retExpr, (NodeToken)sequence.elementAt(2)), retExpr, BinaryExprOp.JOIN_SQBRACKETS, innerExpr);
                        break;
                        case 1: // <DOT> BracketOrDotExprCST
                        Expr rightExpr = (Expr)sequence.elementAt(1).accept(this,null);
                        retExpr = new BinaryExpr(new Location(retExpr,rightExpr), retExpr, BinaryExprOp.JOIN_DOT, rightExpr);
                        break;
                    }
                }
                // now, fix associativity
                retExpr = _makeLeftAssociative((BinaryExpr)retExpr);
                // only flip brackets at top-level, after all associativity is handled
                if (myBracketTopLevel) {
                    // finally, flip bracket exprs
                    // System.out.println(retExpr);
                    _flipBrackets(retExpr);
                }
                break;
            }
            _bracketTopLevel = myBracketTopLevel;
        }
        return retExpr;
    }

    /**
     * @param retExpr
     */
    private void _flipBrackets(Expr expr_) {
        if (expr_ instanceof BinaryExpr) {
            BinaryExpr retExpr = (BinaryExpr)expr_;
            Expr left = retExpr.getLeft();
            Expr right = retExpr.getRight();
            if (retExpr.getOp().equals(BinaryExprOp.JOIN_SQBRACKETS)) {
                // System.out.println("flipping " + left + " and " + right);
                retExpr.setLeft(right);
                retExpr.setRight(left);
            }
        }
        for (int i = 0; i < expr_.numChildren(); i++) {
            if (expr_.childAt(i) instanceof Expr) {
              Expr child = (Expr)expr_.childAt(i);
              _flipBrackets((Expr)expr_.childAt(i));
            }
        }
    }


//    /**
//     * <PRE>
//     * domainExprCST -> DomainExprCST()
//     * nodeOptional -> [ ( &lt;DOT&gt; LetExprCST() | &lt;DOT&gt; DotExprCST() ) ]
//     * </PRE>
//     * @param dotExprCST_ the Dot Expr CST node
//     * @param argu_ not used
//     * @return AST {@link Expr}
//     */
//    public Object visit(DotExprCST dotExprCST_, Object argu_) {
//        /***********GET LEFT EXPR*****************************************/
//        Expr leftExpr = (Expr) dotExprCST_.domainExprCST.accept(this, null);
//        Expr retExpr = leftExpr;
//        // see if this actually has a right expr
//        if (dotExprCST_.nodeOptional.present()) {
//            NodeChoice nChoice = (NodeChoice) dotExprCST_.nodeOptional.node;
//            NodeSequence exprNodes = (NodeSequence) nChoice.choice;
//            /***********GET OPERATOR*****************************************/
//            NodeToken token = (NodeToken) exprNodes.elementAt(0);
//            BinaryExprOp op =
//                new BinaryExprOp(
//                    new Location(_fileName, token),
//                    BinaryExprOp.JOIN_DOT);
//            /***********GET RIGHT EXPR*****************************************/
//            Expr rightExpr = (Expr) exprNodes.elementAt(1).accept(this, null);
//            /***********GET LOCATION*****************************************/
//            Location location = new Location(leftExpr, rightExpr);
//            retExpr = new BinaryExpr(location, leftExpr, op, rightExpr);
//            retExpr = _makeLeftAssociative((BinaryExpr) retExpr);
//        }
//        return retExpr;
//    }
//
    /**
     * <PRE>
     * rangeExprCST -> RangeExprCST()
     * nodeOptional -> [ ( &lt;DOMAIN&gt; LetExprCST() | &lt;DOMAIN&gt; DomainExprCST() ) ]
     * </PRE>
     */
    public Object visit(DomainExprCST domExprCST_, Object argu) {
        /***********GET LEFT EXPR*****************************************/
        Expr leftExpr = (Expr) domExprCST_.rangeExprCST.accept(this, null);
        Expr retExpr = leftExpr;
        // see if this actually has a right expr
        if (domExprCST_.nodeOptional.present()) {
            NodeChoice nChoice = (NodeChoice) domExprCST_.nodeOptional.node;
            NodeSequence exprNodes = (NodeSequence) nChoice.choice;
            /***********GET RIGHT EXPR*****************************************/
            Expr rightExpr = (Expr) exprNodes.elementAt(1).accept(this, null);
            /***********GET LOCATION*****************************************/
            Location location = new Location(leftExpr, rightExpr);
            retExpr = new BinaryExpr(location, leftExpr, BinaryExprOp.DOMAINRESTRICT, rightExpr);
        }
        return retExpr;
    }

    /**
     * <PRE>
     * unopExprCST -> UnopExprCST()
     * nodeOptional -> [ ( &lt;RANGE&gt; LetExprCST() | &lt;RANGE&gt; RangeExprCST() ) ]
     * </PRE>
     */
    public Object visit(RangeExprCST rangeExprCST_, Object argu) {
        /***********GET LEFT EXPR*****************************************/
        Expr leftExpr = (Expr) rangeExprCST_.bracketOrDotExprCST.accept(this, null);
        Expr retExpr = leftExpr;
        // see if this actually has a right expr
        if (rangeExprCST_.nodeOptional.present()) {
            NodeChoice nChoice = (NodeChoice) rangeExprCST_.nodeOptional.node;
            NodeSequence exprNodes = (NodeSequence) nChoice.choice;
            /***********GET RIGHT EXPR*****************************************/
            Expr rightExpr = (Expr) exprNodes.elementAt(1).accept(this, null);
            /***********GET LOCATION*****************************************/
            Location location = new Location(leftExpr, rightExpr);
            retExpr = new BinaryExpr(location, leftExpr, BinaryExprOp.RANGERESTRICT, rightExpr);
            retExpr = _makeLeftAssociative((BinaryExpr) retExpr);
        }
        return retExpr;
    }

    /**
     * <PRE>
     * nodeListOptional -> ( UnOpCST() )*
     * nodeChoice -> ( WithOrLetExprCST() | DoubleColonExprCST() )
     * </PRE>
     * @param unopExprCST_ the Unop Expr CST node
     * @param argu_ not used
     * @return AST {@link Expr}
     */
    public Object visit(UnopExprCST unopExprCST_, Object argu_) {

        /***********GET EXPR*****************************************/
        Expr retExpr = (Expr) unopExprCST_.nodeChoice.choice.accept(this, null);

        // only process more if we have unary operators
        if (unopExprCST_.nodeListOptional.present()) {
            Enumeration unaryOpEnum = unopExprCST_.nodeListOptional.elements();
            retExpr = expandUnaryOpTree(unaryOpEnum, retExpr);
        }

        return retExpr;
    }

    /**
     * create a unary expr tree, with the unary operators associating
     * to the right
     * @param unaryOpEnum_ the unary operators
     * @param expr_ an initial base expression to apply the operators to
     * @return the AST {@link Expr}
     */
    private Expr expandUnaryOpTree(Enumeration unaryOpEnum_, Expr expr_) {
        Expr retExpr = expr_;

        if (unaryOpEnum_.hasMoreElements()) {

            /***********GET OPERATOR*****************************************/
            UnaryExprOp unaryOp =
                (UnaryExprOp) ((UnOpCST) unaryOpEnum_.nextElement()).accept(
                    this,
                    null);

            Expr targetExpr = expandUnaryOpTree(unaryOpEnum_, retExpr);
            Location location = new Location(unaryOp, targetExpr);
            retExpr = new UnaryExpr(location, unaryOp, targetExpr);
        }
        return retExpr;
    }

//    /**
//     * <PRE>
//     * otherExprCST -> OtherExprCST()
//     * nodeOptional -> [ ( &lt;DOUBLECOLON&gt; UnopExprCST() | &lt;DOUBLECOLON&gt; WithOrLetExprCST() ) ]
//     * </PRE>
//     * @param doubleColonExprCST_ the doublecolon Expr CST node
//     * @param argu_ not used
//     * @return AST {@link Expr}
//     */
//    public Object visit(DoubleColonExprCST doubleColonExprCST_, Object argu_) {
//        /***********GET LEFT EXPR*****************************************/
//        Expr leftExpr =
//            (Expr) doubleColonExprCST_.otherExprCST.accept(this, null);
//        Expr retExpr = leftExpr;
//        // see if this actually has a right expr
//        if (doubleColonExprCST_.nodeOptional.present()) {
//            NodeChoice nChoice =
//                (NodeChoice) doubleColonExprCST_.nodeOptional.node;
//            NodeSequence exprNodes = (NodeSequence) nChoice.choice;
//            /***********GET OPERATOR*****************************************/
//            NodeToken token = (NodeToken) exprNodes.elementAt(0);
//            BinaryExprOp op =
//                new BinaryExprOp(
//                    new Location(_fileName, token),
//                    BinaryExprOp.JOIN_DOUBLECOLON);
//            /***********GET RIGHT EXPR*****************************************/
//            Expr rightExpr = (Expr) exprNodes.elementAt(1).accept(this, null);
//            /***********GET LOCATION*****************************************/
//            Location location = new Location(leftExpr, rightExpr);
//            retExpr = new BinaryExpr(location, leftExpr, op, rightExpr);
//            retExpr = _makeLeftAssociative((BinaryExpr) retExpr);
//        }
//        return retExpr;
//    }
//
    /**
     * <PRE>
     * nodeChoice -> InvocationBaseCST()
     *       | &lt;LPAREN&gt; ExprCST() &lt;RPAREN&gt;
     *       | &lt;THIS&gt;
     *       | &lt;NONE&gt;
     *       | &lt;UNIV&gt;
     *       | &lt;IDEN&gt;
     *       | &lt;IF&gt; FormulaCST() &lt;THEN&gt; ExprCST() &lt;ELSE&gt; ExprCST()
     *       | &lt;LBRACE&gt; DeclCST() ( &lt;COMMA&gt; DeclCST() )* [ FormulaBodyCST() ] &lt;RBRACE&gt;
     *       | &lt;SIGINT&gt; IntExprCST()
     *       | SigCST()
     *       | SigCST()
     *       | VarCST()
     * </PRE>
     * @param otherExprCST_ the OtherExpr CST node
     * @param argu_ not used
     * @return AST {@link Expr}
     */
    public Object visit(OtherExprCST otherExprCST_, Object argu_) {
        Expr retExpr = null;
        Location location;
        alloy.parse.syntaxtree.Node exprNode = otherExprCST_.nodeChoice.choice;

        // switch on which type of expression we have
        switch (otherExprCST_.nodeChoice.which) {
            case 0 : // InvocationBaseCST
                retExpr = (InvocationExpr) exprNode.accept(this, null);
                break;
            case 1 : // <LPAREN> ExprCST <RPAREN>
                /***********GET EXPR*****************************************/
		NodeSequence nodes = (NodeSequence) exprNode;
                retExpr =
                    (Expr) nodes.elementAt(1).accept(
                        this,
                        null);
		retExpr.setLocation(new Location(retExpr.getLocation().getFileName(),
						 (NodeToken) nodes.elementAt(0),
						 (NodeToken) nodes.elementAt(2)));
                retExpr.setParens(true);
                break;
            case 2 : // <THIS>
                /***********GET LOCATION*****************************************/
                location = new Location(_fileName, (NodeToken) exprNode);

                retExpr =
                    new VariableExpr(
                        location,
                        new Variable(
                            location,
                            new Id(location, "this"),
                            false));
                break;
            case 3 : // <NONE>
                location = new Location(_fileName, (NodeToken) exprNode);
                //                /***********GET TYPE EXPR*****************************************/
                //                Expr typeExpr =
                //                    (Expr) ((NodeSequence) exprNode).elementAt(2).accept(this, null);
                //                location =
                //                    new Location(
                //                        _fileName,
                //                        (NodeToken) ((NodeSequence) exprNode).elementAt(0),
                //                        (NodeToken) ((NodeSequence) exprNode).elementAt(3));
                retExpr = new EmptySetExpr(location, new EmptyExpr());
                break;
            case 4 : // <UNIV>
                location = new Location(_fileName, (NodeToken) exprNode);
                //                /***********GET TYPE EXPR*****************************************/
                //                Expr typeExpr =
                //                    (Expr) ((NodeSequence) exprNode).elementAt(2).accept(this, null);
                //                location =
                //                    new Location(
                //                        _fileName,
                //                        (NodeToken) ((NodeSequence) exprNode).elementAt(0),
                //                        (NodeToken) ((NodeSequence) exprNode).elementAt(3));
                retExpr = new UniversalExpr(location, new SigExpr(_getUnivName()));
                break;
            case 5 : // <IDEN>
                location = new Location(_fileName, (NodeToken) exprNode);
                //                /***********GET TYPE EXPR*****************************************/
                //                Expr typeExpr =
                //                    (Expr) ((NodeSequence) exprNode).elementAt(2).accept(this, null);
                //                location =
                //                    new Location(
                //                        _fileName,
                //                        (NodeToken) ((NodeSequence) exprNode).elementAt(0),
                //                        (NodeToken) ((NodeSequence) exprNode).elementAt(3));
                retExpr = new IdentityExpr(location, new SigExpr(_getUnivName()));
                break;

            case 6 : // if-then-else
                NodeToken ifToken =
                    (NodeToken) ((NodeSequence) exprNode).elementAt(0);
                Formula ifFormula =
                    (Formula) ((NodeSequence) exprNode).elementAt(1).accept(
                        this,
                        null);
                Expr thenExpr =
                    (Expr) ((NodeSequence) exprNode).elementAt(3).accept(
                        this,
                        null);
                Expr elseExpr =
                    (Expr) ((NodeSequence) exprNode).elementAt(5).accept(
                        this,
                        null);
                location = new Location(ifToken, elseExpr);
                retExpr =
                    new IfThenElseExpr(location, ifFormula, thenExpr, elseExpr);
                break;
            case 7 : // set comprehension
                Enumeration compNodes = ((NodeSequence) exprNode).elements();
                // keep left brace for location
                NodeToken leftBrace = (NodeToken) compNodes.nextElement();

                /***********GET DECLS*****************************************/
                Decls decls = createDecls(compNodes);
                // see if formula exists exists
                Formula formula = new EmptyFormula();
                NodeOptional formulaNode =
                    (NodeOptional) compNodes.nextElement();
                if (formulaNode.present()) {
                    /***********GET FORMULA*****************************************/
                    formula = (Formula) formulaNode.node.accept(this, null);
                }
                // keep right brace for location
                NodeToken rightBrace = (NodeToken) compNodes.nextElement();
                location = new Location(_fileName, leftBrace, rightBrace);

                retExpr =
                    new ComprehensionExpr(location, decls, formula, false);
                break;
            case 8 : // <SIGINT> IntExprCST
                /***********GET INT EXPR*****************************************/
                IntExpr intExpr =
                    (IntExpr) ((NodeSequence) exprNode).elementAt(1).accept(
                        this,
                        null);

		// lazily import alloy/lang/Int
		_importInt();

                retExpr =
                    new IntExprCastExpr(
                        new Location(
                            (NodeToken) ((NodeSequence) exprNode).elementAt(0),
                            intExpr),
                        intExpr);
                break;

            case 9 :
            case 10 : // SigCST
                SigExpr sigExpr = (SigExpr) exprNode.accept(this, null);
                retExpr = sigExpr;
                break;
            case 11 : // VarCST
                /***********GET VARIABLE*****************************************/
                Variable var = (Variable) exprNode.accept(this, null);

                retExpr = new VariableExpr(var.getLocation(), var);
                break;
            default :
                Dbg.chk(false);
        }
        return retExpr;
    }

    /**
     * <PRE>
     * paraNameCST -> ParaNameCST()
     * nodeToken -> &lt;LPAREN&gt;
     * nodeOptional -> [ ExprCST() ( &lt;COMMA&gt; ExprCST() )* ]
     * nodeToken1 -> &lt;RPAREN&gt;
     * </PRE>
     * @param invocationBaseCST_ the Invocation Base CST node
     * @param argu_ not used
     * @return AST {@link InvocationExpr}
     */
    public Object visit(InvocationBaseCST invocationBaseCST_, Object argu_) {

        /***********GET NAME*****************************************/
        QualifiedName name =
            (QualifiedName) invocationBaseCST_.paraNameCST.accept(this, null);

        // check if there are any args
        Exprs args = new Exprs();
        if (invocationBaseCST_.nodeOptional.present()) {
            /***********GET EXPRS*****************************************/
            Enumeration argEnum =
                ((NodeSequence) invocationBaseCST_.nodeOptional.node)
                    .elements();
            args = createExprs(argEnum);
        }

        /***********GET LOCATION*****************************************/
        Location location = new Location(name, invocationBaseCST_.nodeToken1);

        return new InvocationExpr(location, new EmptyExpr(), name, args);
    }

    /**
     * <PRE>
     * sigNameCST -> SigNameCST()
     * </PRE>
     * @param sigCST_ the Sig CST node
     * @param argu_ not used
     * @return AST {@link SigExpr}
     */
    public Object visit(SigCST sigCST_, Object argu_) {

    QualifiedName name = (QualifiedName) sigCST_.sigNameCST.accept(this, null);
    // if the name of the sig is "Int," lazily import alloy/lang/Int into
    // the module
    if (name.getId().equals(new Id(INT))) _importInt();
    return new SigExpr(name.getLocation(), name);
    }

    /**
     * <PRE>
     * nodeChoice -> &lt;PLUS&gt; | &lt;MINUS&gt;
     * </PRE>
     * @param unionDiffOpCST_ the UnionDiffOpCST node
     * @param argu_ not used
     * @return AST {@link BinaryExprOp}
     */
    public Object visit(UnionDiffOpCST unionDiffOpCST_, Object argu_) {
        switch (unionDiffOpCST_.nodeChoice.which) {
        case 0: return BinaryExprOp.UNION;
        case 1: return BinaryExprOp.DIFF;
        default: Dbg.chk("no such unionDiffOpCST"); return null;
        }
    }

    /**
     * <PRE>
     * nodeChoice -> &lt;TILDE&gt; | &lt;STAR&gt; | &lt;CARET&gt;
     * </PRE>
     * @param unOpCST_ the UnOpCST node
     * @param argu_ not used
     * @return AST {@link UnaryExprOp}
     */
    public Object visit(UnOpCST unOpCST_, Object argu_) {
        switch (unOpCST_.nodeChoice.which) {
        case 0: return UnaryExprOp.TRANSPOSE;
        case 1: return UnaryExprOp.REF_TRANS_CLOSURE;
        case 2: return UnaryExprOp.TRANS_CLOSURE;
        default: Dbg.fail("no such UnOpCST"); return null;
        }
    }

    /****************************************************************
     *                    INTEXPR STUFF                             *
     *                                                              *
     * all convert to type IntExpr                                  *
     * SumWithOrLetIntExprCST                                          *
     * BinaryIntExprCST                                             *
     * IntExprCST                                                   *
     * OtherIntExprCST                                              *
     *                                                              *
     *                                                              *
     * IntOpCST => IntExprOp                                        *
     *                                                              *
     ****************************************************************/

    /**
     * <PRE>
     * nodeChoice -> SumWithOrLetIntExprCST()
     *       | BinaryIntExprCST()
     * </PRE>
     * @param intExprCST_ the IntExprCST node
     * @param argu_ not used
     * @return AST {@link IntExpr}
     */
    public Object visit(IntExprCST intExprCST_, Object argu_) {
        // just visit the child and return the result
        return intExprCST_.nodeChoice.choice.accept(this, null);

    }

    /**
     * <PRE>
     * nodeChoice -> &lt;SUM&gt; DeclCST() ( &lt;COMMA&gt; DeclCST() )* &lt;BAR&gt; IntExprCST()
     *       | &lt;LET&gt; LetDeclCST() ( &lt;COMMA&gt; LetDeclCST() )* &lt;BAR&gt; IntExprCST()
     * </PRE>
     * @param sumOrWithIntExprCST_ the SumWithOrLetIntExprCST node
     * @param argu_ not used
     * @return AST {@link IntExpr}
     */

    public Object visit(SumOrLetIntExprCST sumOrLetIntExprCST_, Object argu_) {
        alloy.parse.syntaxtree.Node choice =
            sumOrLetIntExprCST_.nodeChoice.choice;
        IntExpr retExpr = null;
        // switch on node choice
        switch (sumOrLetIntExprCST_.nodeChoice.which) {
            case 0 : // <SUM> DeclCST ( <COMMA> DeclCST )* <BAR> IntExprCST
                NodeSequence sumSequence = (NodeSequence) choice;
                // get <SUM> token for location
                NodeToken sumToken = (NodeToken) sumSequence.elementAt(0);

                /***********GET DECLS*****************************************/
                // create a new Vector to have an enumeration
                // of declCST node and nodeListOptional for createDecls()
                // method
                Vector tempVec = new Vector();
                tempVec.addElement(sumSequence.elementAt(1));
                tempVec.addElement(sumSequence.elementAt(2));
                Decls decls = createDecls(tempVec.elements());

                /***********GET EXPR*****************************************/
                IntExpr sumExpr =
                    (IntExpr) sumSequence.elementAt(4).accept(this, null);

                /***********GET LOCATION*****************************************/
                Location location = new Location(sumToken, sumExpr);

                retExpr = new SumIntExpr(location, decls, sumExpr);
                break;
            case 1 : // <LET> LetDeclCST ( <COMMA> LetDeclCST )* <BAR> IntExprCST
                Enumeration enum2 = ((NodeSequence) choice).elements();

                NodeToken letToken = (NodeToken) enum2.nextElement();
                LetDecls letDecls = createLetDecls(enum2);
                enum2.nextElement();
                IntExpr body =
                    (IntExpr)
                        (
                            (alloy.parse.syntaxtree.Node) enum2
                                .nextElement())
                                .accept(
                        this,
                        null);
                location = new Location(letToken, body);
                retExpr = new LetIntExpr(location, letDecls, body);
                break;
        }
        return retExpr;
    }

    /**
     * <PRE>
     * otherIntExprCST -> OtherIntExprCST()
     * nodeOptional -> [ ( IntOpCST() BinaryIntExprCST() | IntOpCST() SumWithOrLetIntExprCST() ) ]
     * </PRE>
     * @param binaryIntExprCST_ the BinaryIntExprCST node
     * @param argu_ Boolean flag indicating whether to associate to the left (true) or 
     *              right (false).  If argu_ is null, the method associates to the left.
     * @return AST {@link IntExpr}
     */
    public Object visit(BinaryIntExprCST binaryIntExprCST_, Object argu_) {

        /***********GET LEFT EXPR*****************************************/
        IntExpr leftExpr =
            (IntExpr) binaryIntExprCST_.otherIntExprCST.accept(this, null);
        IntExpr retExpr = leftExpr;
        if (binaryIntExprCST_.nodeOptional.present()) {
            NodeSequence binaryIntExprNodes =
                (NodeSequence)
                    ((NodeChoice) binaryIntExprCST_.nodeOptional.node).choice;
            /***********GET OPERATOR*****************************************/
            IntExprOp op =
                (IntExprOp)
                    ((IntOpCST) binaryIntExprNodes.elementAt(0)).accept(
                    this,
                    null);

            /***********GET RIGHT EXPR*****************************************/
            IntExpr rightExpr =
                (IntExpr)
                    (
                        (
                            alloy
                                .parse
                                .syntaxtree
                                .Node) binaryIntExprNodes
                                .elementAt(
                            1)).accept(
                    this,
                    Boolean.FALSE); // if the right child is also a binary formula
                                    // its children should NOT associate to the left; the
                                    // algorithm below will work only if its children 
                                    // associate to the right.

            /***********GET LOCATION*****************************************/
            Location location = new Location(leftExpr, rightExpr);

            // this makes integer operations left associative:  ugly hack :(
            if ((argu_ == null || ((Boolean)argu_).booleanValue()) && 
                rightExpr instanceof BinaryIntExpr) {
                BinaryIntExpr binRightExpr = (BinaryIntExpr) rightExpr;
                Location binLeftExprLocation = new Location(leftExpr, binRightExpr.getLeft());
                BinaryIntExpr binLeftExpr = new BinaryIntExpr(binLeftExprLocation, leftExpr, 
                                                              op, binRightExpr.getLeft());
                
                while (binRightExpr.getRight() instanceof BinaryIntExpr) {
                    BinaryIntExpr tempRightExpr = (BinaryIntExpr) binRightExpr.getRight();
                    binLeftExprLocation = new Location(leftExpr, tempRightExpr.getLeft());
                    binLeftExpr = new BinaryIntExpr(binLeftExprLocation, binLeftExpr, 
                                                    binRightExpr.getOp(), 
                                                    tempRightExpr.getLeft());
         
                    binRightExpr = tempRightExpr;
                }
                
                retExpr = new BinaryIntExpr(location, binLeftExpr, binRightExpr.getOp(),
                                            binRightExpr.getRight());
            } else {
                retExpr = new BinaryIntExpr(location, leftExpr, op, rightExpr);
            }
            
        }
        
        return retExpr;
    }

    /**
     * <PRE>
     * nodeChoice -> &lt;NUMBER&gt;
     *       | &lt;IF&gt; FormulaCST() &lt;THEN&gt; IntExprCST() &lt;ELSE&gt; IntExprCST()
     *       | &lt;HASH&gt; ExprCST()
     *       | &lt;SUM&gt; ExprCST()
     *       | &lt;INT&gt; ExprCST()
     *       | &lt;LPAREN&gt; IntExprCST() &lt;RPAREN&gt;
     * </PRE>
     * @param otherIntExprCST_ the OtherIntExprCST node
     * @param argu_ not used
     * @return AST {@link IntExpr}
     */
    public Object visit(OtherIntExprCST otherIntExprCST_, Object argu_) {
        IntExpr retExpr = null;
        Location location;
        alloy.parse.syntaxtree.Node exprNode =
            otherIntExprCST_.nodeChoice.choice;

        switch (otherIntExprCST_.nodeChoice.which) {
            case 0 : // <NUMBER>
                /***********GET NUMBER*****************************************/
                int val = Integer.parseInt(((NodeToken) exprNode).tokenImage);
                retExpr =
                    new LiteralIntExpr(
                        new Location(_fileName, (NodeToken) exprNode),
                        val);
                break;
            case 1 : // if-then-else
                NodeToken ifToken =
                    (NodeToken) ((NodeSequence) exprNode).elementAt(0);
                Formula ifFormula =
                    (Formula) ((NodeSequence) exprNode).elementAt(1).accept(
                        this,
                        null);
                IntExpr thenIntExpr =
                    (IntExpr) ((NodeSequence) exprNode).elementAt(3).accept(
                        this,
                        null);
                IntExpr elseIntExpr =
                    (IntExpr) ((NodeSequence) exprNode).elementAt(5).accept(
                        this,
                        null);
                location = new Location(ifToken, elseIntExpr);
                retExpr =
                    new IfThenElseIntExpr(
                        location,
                        ifFormula,
                        thenIntExpr,
                        elseIntExpr);
                break;
            case 2 : // <HASH> ExprCST
                // get <HASH> token for location
                NodeToken hashToken =
                    (NodeToken) ((NodeSequence) exprNode).elementAt(0);

                /***********GET CARDINALITY EXPR BODY*****************************************/
                Expr cardBody =
                    (Expr) ((NodeSequence) exprNode).elementAt(1).accept(
                        this,
                        null);

                /***********GET LOCATION*****************************************/
                location = new Location(hashToken, cardBody);

                retExpr = new CardinalityExpr(location, cardBody);
                break;
            case 3 : // <SUM> ExprCST
                // get <SUM> token for location
                NodeToken sumToken =
                    (NodeToken) ((NodeSequence) exprNode).elementAt(0);

                /***********GET SUM EXPR BODY*****************************************/
                Expr sumBody =
                    (Expr) ((NodeSequence) exprNode).elementAt(1).accept(
                        this,
                        null);

                /***********GET LOCATION*****************************************/
                location = new Location(sumToken, sumBody);

		// lazily import alloy/lang/Int
		_importInt();

                retExpr = new SumExpr(location, sumBody);
                break;
            case 4 : // <INT> ExprCST
                // get <INT> token for location
                NodeToken intToken =
                    (NodeToken) ((NodeSequence) exprNode).elementAt(0);

                /***********GET EXPR BODY*****************************************/
                Expr intBody =
                    (Expr) ((NodeSequence) exprNode).elementAt(1).accept(
                        this,
                        null);

                /***********GET LOCATION*****************************************/
                location = new Location(intToken, intBody);

		// lazily import alloy/lang/Int
		_importInt();

                retExpr = new ExprCastIntExpr(location, intBody);
                break;
            case 5 : // <LPAREN> IntExprCST <RPAREN>
                retExpr =
                    (IntExpr) ((NodeSequence) exprNode).elementAt(1).accept(
                        this,
                        null);
		// include parens in location
		retExpr.setLocation(new Location(retExpr.getLocation().getFileName(),
						 (NodeToken) ((NodeSequence) exprNode).elementAt(0),
						 (NodeToken) ((NodeSequence) exprNode).elementAt(2)));
                break;
        }

        return retExpr;
    }

    /**
     * <PRE>
     * nodeChoice -> &lt;PLUS&gt; | &lt;MINUS&gt;
     * </PRE>
     * @param intOpCST_ the IntOpCST node
     * @param argu_ not used
     * @return AST {@link IntExprOp}
     */
    public Object visit(IntOpCST intOpCST_, Object argu_) {
        switch(intOpCST_.nodeChoice.which) {
        	case 0: return IntExprOp.PLUS;
        	case 1: return IntExprOp.MINUS;
        	default: Dbg.chk(false); return null;
        }
    }

    /****************************************************************
     *                    FORMULA STUFF                             *
     *                                                              *
     * all convert to type Formula                                  *
     * FormulaBodyCST                                               *
     * FormulaCST                                                   *
     * QuantWithOrLetFormulaCST                                     *
     * OrFormulaCST                                                 *
     * EquivalenceFormulaCST                                        *
     * ImplicationFormulaCST                                        *
     * AndFormulaCST                                                *
     * OtherFormulaCST                                              *
     *                                                              *
     * all convert to type LogicOp                                  *
     * OrOpCST                                                      *
     * EquivOpCST                                                   *
     * AndOpCST                                                     *
     *                                                              *
     * QuantifierCST => Quantifier                                  *
     * IntCompOpCST  => IntCompOp                                   *
     *                                                              *
     ****************************************************************/

    /**
     * <PRE>
     * nodeChoice -> FormulaSeqCST()
     *       | &lt;BAR&gt; FormulaCST()
     * @param formulaBodyCST_, the FormulaBodyCST node
     * @param argu_ not used
     * @return AST {@link Formula}
     */
    public Object visit(FormulaBodyCST formulaBodyCST_, Object argu_) {
        Formula retFormula = new EmptyFormula();
        alloy.parse.syntaxtree.Node formulaNode =
            formulaBodyCST_.nodeChoice.choice;

        // switch on which production we have
        switch (formulaBodyCST_.nodeChoice.which) {
            case 0 : // FormulaSeqCST
                retFormula = (Formula) formulaNode.accept(this, null);
                break;
            case 1 : // <BAR> FormulaCST
                retFormula =
                    (Formula) ((NodeSequence) formulaNode).elementAt(1).accept(
                        this,
                        null);
                break;
        }

        return retFormula;
    }

    /**
     * <PRE>
     * nodeChoice -> QuantWithOrLetFormulaCST()
     *       | OrFormulaCST()
     * </PRE>
     * @param formulaCST_, the FormulaCST node
     * @param argu_ not used
     * @return AST {@link Formula}
     */
    public Object visit(FormulaCST formulaCST_, Object argu_) {

        // just visit the child and return the result
        return formulaCST_.nodeChoice.choice.accept(this, null);
    }

    /**
     * <PRE>
     * nodeChoice -> QuantifierCST() DeclCST() ( &lt;COMMA&gt; DeclCST() )* FormulaBodyCST()
     *       | &lt;LET&gt; LetDeclCST() ( &lt;COMMA&gt; LetDeclCST() )* FormulaBodyCST()
     * </PRE>
     * @param quantOrWithFormulaCST_, the QuantWithOrLetFormulaCST node
     * @param argu_ not used
     * @return AST {@link Formula}
     */
    public Object visit(
        QuantOrLetFormulaCST quantOrLetFormulaCST_,
        Object argu_) {
        Formula retFormula = null;
        Location location;
        Enumeration formulaEnum =
            ((NodeSequence) quantOrLetFormulaCST_.nodeChoice.choice).elements();

        // switch on which production we have
        switch (quantOrLetFormulaCST_.nodeChoice.which) {
            case 0 : // quantified formula
                /*********GET QUANTIFIER*******************************/
                Quantifier quantifier =
                    (Quantifier)
                        ((QuantifierCST) formulaEnum.nextElement()).accept(
                        this,
                        null);

                /*********GET DECLS*******************************/
                Decls decls = createDecls(formulaEnum);

                /*********GET FORMULA*******************************/
                Formula quantBody =
                    (Formula)
                        ((FormulaBodyCST) formulaEnum.nextElement()).accept(
                        this,
                        null);

                /*********GET LOCATION*******************************/
                location = new Location(quantifier, quantBody);

                retFormula =
                    new QuantifiedFormula(
                        location,
                        quantifier,
                        decls,
                        quantBody,
                        false);
                break;
            case 1 : // let formula
                NodeToken letToken = (NodeToken) formulaEnum.nextElement();
                LetDecls letDecls = createLetDecls(formulaEnum);
                Formula body =
                    (Formula)
                        (
                            (alloy.parse.syntaxtree.Node) formulaEnum
                                .nextElement())
                                .accept(
                        this,
                        null);
                location = new Location(letToken, body);
                retFormula = new LetFormula(location, letDecls, body);
                break;

        }

        return retFormula;
    }

    /**
     * <PRE>
     * equivalenceFormulaCST -> EquivalenceFormulaCST()
     * nodeOptional -> [ ( OrOpCST() QuantWithOrLetFormulaCST() | OrOpCST() OrFormulaCST() ) ]
     * </PRE>
     * @param orFormulaCST_ the OrFormulaCST node
     * @param argu_ not used
     * @return AST {@link Formula}
     */
    public Object visit(OrFormulaCST orFormulaCST_, Object argu_) {
        /*********GET LEFT FORMULA*****************************/
        Formula retFormula =
            (Formula) orFormulaCST_.equivalenceFormulaCST.accept(this, null);
        if (orFormulaCST_.nodeOptional.present()) {
            NodeSequence orNodes =
                (NodeSequence)
                    ((NodeChoice) orFormulaCST_.nodeOptional.node).choice;

            /*********GET OPERATOR*****************************/
            LogicOp op = (LogicOp) orNodes.elementAt(0).accept(this, null);

            /*********GET RIGHT FORMULA*****************************/
            Formula rightFormula =
                (Formula) orNodes.elementAt(1).accept(this, null);

            /*********GET LOCATION*****************************/
            Location location = new Location(retFormula, rightFormula);

            retFormula =
                new BinaryFormula(location, retFormula, op, rightFormula);
        }

        return retFormula;
    }

    /**
     * <PRE>
     * implicationFormulaCST -> ImplicationFormulaCST()
     * nodeOptional -> [ ( EquivOpCST() EquivalenceFormulaCST() | EquivOpCST() QuantWithOrLetFormulaCST() ) ]
     * </PRE>
     * @param equivalenceFormulaCST_ the EquivalenceFormulaCST node
     * @param argu_ not used
     * @return AST {@link Formula}
     */
    public Object visit(
        EquivalenceFormulaCST equivalenceFormulaCST_,
        Object argu_) {
        /*********GET LEFT FORMULA*****************************/
        Formula retFormula =
            (Formula) equivalenceFormulaCST_.implicationFormulaCST.accept(
                this,
                null);
        if (equivalenceFormulaCST_.nodeOptional.present()) {
            NodeSequence orNodes =
                (NodeSequence)
                    (
                        (
                            NodeChoice) equivalenceFormulaCST_
                                .nodeOptional
                                .node)
                                .choice;

            /*********GET OPERATOR*****************************/
            LogicOp op = (LogicOp) orNodes.elementAt(0).accept(this, null);

            /*********GET RIGHT FORMULA*****************************/
            Formula rightFormula =
                (Formula) orNodes.elementAt(1).accept(this, null);

            /*********GET LOCATION*****************************/
            Location location = new Location(retFormula, rightFormula);

            retFormula =
                new BinaryFormula(location, retFormula, op, rightFormula);
        }

        return retFormula;
    }

    /**
     * <PRE>
     * nodeChoice -> AndFormulaCST() ImpliesOpCST() QuantWithOrLetFormulaCST()
     *       | AndFormulaCST() ImpliesOpCST() ImplicationFormulaCST() [ ElseOpCST() FormulaCST() ]
     *       | AndFormulaCST()
     * </PRE>
     * @param implicationFormulaCST_ the ImplicationFormulaCST node
     * @param argu_ not used
     * @return AST {@link Formula}
     */
    public Object visit(
        ImplicationFormulaCST implicationFormulaCST_,
        Object argu_) {
        Formula retFormula = null, ifFormula, thenFormula, elseFormula;
        Location location;
        alloy.parse.syntaxtree.Node impNode =
            implicationFormulaCST_.nodeChoice.choice;
        NodeSequence seq;
        switch (implicationFormulaCST_.nodeChoice.which) {
            case 0 : // AndFormulaCST ImpliesOpCST QuantWithOrLetFormulaCST
                seq = (NodeSequence) impNode;
                ifFormula = (Formula) seq.elementAt(0).accept(this, null);
                thenFormula = (Formula) seq.elementAt(2).accept(this, null);
                location = new Location(ifFormula, thenFormula);
                retFormula =
                    new ImplicationFormula(
                        location,
                        ifFormula,
                        thenFormula,
                        new EmptyFormula());
                break;
            case 1 : // AndFormulaCST ImpliesOpCST ImplicationFormulaCST [ ElseOpCST FormulaCST ]
                seq = (NodeSequence) impNode;
                ifFormula = (Formula) seq.elementAt(0).accept(this, null);
                thenFormula = (Formula) seq.elementAt(2).accept(this, null);
                // see which production we have at the end
                NodeOptional opt = (NodeOptional) seq.elementAt(3);
                if (opt.present()) {
                    NodeSequence elseSeq = (NodeSequence) opt.node;
                    elseFormula =
                        (Formula) elseSeq.elementAt(1).accept(this, null);
                    location = new Location(ifFormula, elseFormula);
                    retFormula =
                        new ImplicationFormula(
                            location,
                            ifFormula,
                            thenFormula,
                            elseFormula);
                } else {
                    location = new Location(ifFormula, thenFormula);
                    retFormula =
                        new ImplicationFormula(
                            location,
                            ifFormula,
                            thenFormula,
                            new EmptyFormula());
                }
                break;
            case 2 : // AndFormulaCST
                retFormula = (Formula) impNode.accept(this, null);
                break;
        }
        return retFormula;
    }

    /**
     * <PRE>
     * otherFormulaCST -> OtherFormulaCST()
     * nodeOptional -> [ ( AndOpCST() AndFormulaCST() | AndOpCST() QuantWithOrLetFormulaCST() ) ]
         * </PRE>
     * @param andFormulaCST_ the AndFormulaCST node
     * @param argu_ not used
     * @return AST {@link Formula}
     */
    public Object visit(AndFormulaCST andFormulaCST_, Object argu_) {
        /*********GET LEFT FORMULA*****************************/
        Formula retFormula =
            (Formula) andFormulaCST_.otherFormulaCST.accept(this, null);
        if (andFormulaCST_.nodeOptional.present()) {
            NodeSequence orNodes =
                (NodeSequence)
                    ((NodeChoice) andFormulaCST_.nodeOptional.node).choice;

            /*********GET OPERATOR*****************************/
            LogicOp op = (LogicOp) orNodes.elementAt(0).accept(this, null);

            /*********GET RIGHT FORMULA*****************************/
            Formula rightFormula =
                (Formula) orNodes.elementAt(1).accept(this, null);

            /*********GET LOCATION*****************************/
            Location location = new Location(retFormula, rightFormula);

            retFormula =
                new BinaryFormula(location, retFormula, op, rightFormula);
        }

        return retFormula;
    }



    /**
     * Requires nseq = QuantifierCST() ExprCST()
     * @return QuantifiedExpr corresponding to nseq
     **/
    private QuantifiedExpr getQuantifiedExpr(NodeSequence nseq) {

    /**********GET QUANTIFIER***********************/
    Quantifier quantifier =
        (Quantifier) nseq.elementAt(0).accept(this, null);

    /**********GET EXPR***********************/
    Expr expr =
        (Expr) nseq.elementAt(1).accept(this, null);

    QuantifiedExpr quantExpr =
        new QuantifiedExpr(new Location(quantifier, expr),
                   quantifier, expr);

    // EMINA: all expr is now disallowed
    if (quantifier.equals(Quantifier.ALL)) {
        error("all is not valid for a quantified expression", quantExpr);
    }

    return quantExpr;
    }

    /**
     * Requires nseq = IntExprCST() IntCompOpCST() IntExprCST()
     * @return ElemIntFormula corresponding to nseq
     **/
    private ElemIntFormula getElemIntFormula(NodeSequence nseq) {
    /**********GET LEFT INTEXPR***********************/
    IntExpr leftIntExpr =
        (IntExpr) nseq.elementAt(0).accept(this, null);

    /**********GET COMP OP***********************/
    IntCompOp intCompOp =
        (IntCompOp) nseq.elementAt(1).accept(this, null);

    /**********GET RIGHT EXPR***********************/
    IntExpr rightIntExpr =
        (IntExpr) nseq.elementAt(2).accept(this,null);

    return new ElemIntFormula(new Location(leftIntExpr, rightIntExpr),
                  leftIntExpr, intCompOp, rightIntExpr);

    }

    /**
     * Requires nseq = ExprCST() &lt;COLON&gt; MultExprCST()
     * @return MultiplicityFormula corresponding to nseq
     **/
    private MultiplicityFormula getMultiplicityFormula(NodeSequence nseq) {
    /**********GET LEFT EXPR***********************/
    Expr expr =
        (Expr) nseq.elementAt(0).accept(this, null);

    /**********GET RIGHT MULT_EXPR***********************/
    MultiplicityExpr multExpr =
        (MultiplicityExpr) nseq.elementAt(2).accept(this, null);

    return new MultiplicityFormula(new Location(expr, multExpr),
                       expr, multExpr);

    }

    /**
     * Requires nseq = ExprCST() CompOpCST() ExprCST()
     * @return ElemFormula corresponding to nseq
     **/
    private ElemFormula getElemFormula(NodeSequence nseq) {
    /**********GET LEFT EXPR***********************/
    Expr leftExpr = (Expr) nseq.elementAt(0).accept(this,null);

    /**********GET COMP OP***********************/
    CompOp compOp = (CompOp) nseq.elementAt(1).accept(this,null);

    /**********GET RIGHT EXPR***********************/
    Expr rightExpr = (Expr) nseq.elementAt(2).accept(this, null);

    return new ElemFormula(new Location(leftExpr, rightExpr),
                   leftExpr, compOp, rightExpr);

    }

    /**
     * Requires node = InvocationExprCST()
     * @return InvocationFormula corresponding to node
     **/
    private Formula getInvocationFormula(Node node) {
    // even though the production is for an invocation expr,
    // we aren't guaranteed to have an invocation
    Expr tempExpr = (Expr) node.accept(this, null);
    if (tempExpr instanceof InvocationExpr) {
        InvocationExpr invocation =
        (InvocationExpr) node.accept(this, null);
        return new InvocationFormula(invocation.getLocation(),
                     invocation.getReceiver(),
                     invocation.getInvocableName(),
                     invocation.getExprs());
    } else {
        error("use of non-invocation expression as formula (check parens / operator precedence)", tempExpr);
        return new EmptyFormula();
    }

    }

    /**
     * Requires nseq = NegOpCST() OtherFormulaCST()
     * @return NegFormula corresponding to nseq
     **/
    private NegFormula getNegFormula(NodeSequence nseq) {
    /********GET FORMULA**********************/
    Formula negatedFormula =
        (Formula) nseq.elementAt(1).accept(this, null);

    // get negation token for location
    NodeToken negToken =
        (NodeToken) ((NegOpCST) nseq.elementAt(0)).nodeChoice.choice;

    return new NegFormula(new Location(negToken, negatedFormula),
                  negatedFormula);
    }

   /**
    * <PRE>
    * nodeChoice -> QuantifierCST() ExprCST()
    *       | IntExprCST() IntCompOpCST() IntExprCST()
    *       | ExprCST() &lt;COLON&gt; MultExprCST()
    *       | ExprCST() CompOpCST() ExprCST()
    *       | InvocationExprCST()
    *       | InvocationExprCST()
    *       | &lt;LPAREN&gt; FormulaCST() &lt;RPAREN&gt;
    *       | FormulaSeqCST()
    *       | NegOpCST() OtherFormulaCST()
    * </PRE>
    * @param otherFormulaCST_ the OtherFormulaCST node
    * @param argu_ not used
    * @return AST {@link Formula}
    */
    public Object visit(OtherFormulaCST otherFormulaCST_, Object argu_) {
        Formula retFormula = null;
        alloy.parse.syntaxtree.Node choiceNode =
            otherFormulaCST_.nodeChoice.choice;

        // switch on which production we have
        switch (otherFormulaCST_.nodeChoice.which) {
            case 0 : // QuantifierCST ExprCST
        retFormula = getQuantifiedExpr((NodeSequence) choiceNode);
                break;
            case 1 : // IntExprCST IntCompOpCST IntExprCST
        retFormula = getElemIntFormula((NodeSequence) choiceNode);
                break;
        case 2 : // ExprCST() &lt;COLON&gt; MultExprCST()
        retFormula = getMultiplicityFormula((NodeSequence) choiceNode);
                break;
            case 3 : // ExprCST CompOpCST ExprCST
        retFormula = getElemFormula((NodeSequence) choiceNode);
                break;
            case 4 :
            case 5 : // InvocationExprCST
        retFormula = getInvocationFormula(choiceNode);
                break;
            case 6 : // <LPAREN> FormulaCST <RPAREN>
                retFormula =
                    (Formula)
		    ((NodeSequence) choiceNode).elementAt(1).accept(this,null);
		Node leftParens = ((NodeSequence) choiceNode).elementAt(0);
		Node rightParens = ((NodeSequence) choiceNode).elementAt(2);

		((TreeNode)retFormula).setLocation(new Location(retFormula.getLocation().getFileName(),
								(NodeToken)leftParens, 
								(NodeToken)rightParens));
                break;
            case 7 : // FormulaSeqCST
                // just visit the node
                retFormula = (Formula) choiceNode.accept(this, null);
                break;
            case 8 : // NegOpCST FormulaCST
                retFormula = getNegFormula((NodeSequence) choiceNode);
                break;
        }

        return retFormula;
    }

    /**
     * <PRE>
     * nodeChoice -> &lt;DOUBLEAMPERSAND&gt;| &lt;AND&gt;
     * </PRE>
     * @param andOpCST_ the And Operator node
     * @param argu_ not used
     * @return AST {@link LogicOp}
     */
    public Object visit(AndOpCST andOpCST_, Object argu) {
        return LogicOp.AND;
    }

    /**
     * <PRE>
     * nodeChoice -> &lt;DOUBLEBAR&gt;
     *       | &lt;OR&gt;
     * </PRE>
     * @param orOpCST_ the Or Operator node
     * @param argu_ not used
     * @return AST {@link LogicOp}
     */
    public Object visit(OrOpCST orOpCST_, Object argu) {
        return LogicOp.OR;
    }

    /**
     * <PRE>
     * nodeChoice -> &lt;EQUIVARROW&gt;| &lt;IFF&gt;
     * </PRE>
     * @param equivOpCST_ the Equiv Operator node
     * @param argu_ not used
     * @return AST {@link LogicOp}
     */
    public Object visit(EquivOpCST equivOpCST_, Object argu) {
        return LogicOp.IFF;
    }

    /**
     * <PRE>
     * nodeOptional -> [ NegOpCST() ]
     * nodeChoice -> ( &lt;EQUALS&gt; | &lt;LTE&gt; | &lt;GTE&gt; | &lt;LT&gt; | &lt;GT&gt; )
     * </PRE>
     * @param intCompOpCST_ the Comp. Op. CST node
     * @param argu_ not used
     * @return AST {@link IntCompOp}
     */
    public Object visit(IntCompOpCST intCompOpCST_, Object argu_) {

        /***********GET NEGATION*****************************************/
        boolean neg = intCompOpCST_.nodeOptional.present();

        /***********GET OPCODE*****************************************/
        // dependent on which, but easy
        switch(intCompOpCST_.nodeChoice.which) {
        	case 0: return !neg ? IntCompOp.INT_EQUALS : IntCompOp.INT_NOTEQUALS;
        	case 1: return !neg ? IntCompOp.INT_LTE    : IntCompOp.INT_GT;
        	case 2: return !neg ? IntCompOp.INT_GTE    : IntCompOp.INT_LT;
        	case 3: return !neg ? IntCompOp.INT_LT     : IntCompOp.INT_GTE;
        	case 4: return !neg ? IntCompOp.INT_GT     : IntCompOp.INT_LTE;
        	default: Dbg.fatal("no such intCompOpCST"); return null;
        }
    }

    private class NonInvocationException extends Exception {
    }

    /****************************************************************
     *                COMMANDS, SCOPE, ETC                          *
     *                                                              *
     *  RunCST        => RunCommand                                 *
     *  CheckCST      => CheckCommand                               *
     *  ScopeCST      => Scope                                      *
     *  TypeScopeCST  => TypeScope                                  *
     *                                                              *
     *                                                              *
     ****************************************************************/
    
    /**
     * <PRE>
     * nodeOptional -> [ &lt;ID&gt; &lt;COLON&gt; ]
     * nodeToken -> &lt;RUN&gt;
     * paraNameCST -> ParaNameCST()
     * nodeOptional1 -> [ ScopeCST() ]
     * nodeOptional2 -> [ &lt;EXPECT&gt; &lt;NUMBER&gt; ]
     * </PRE>
     * @param runCST_, run Command node of the CST
     * @param argu_ not used
     * @return AST {@link RunCommand}
     */
    public Object visit(RunCST runCST_, Object argu_) {

        /***********GET NAME*****************************************/
        String name = null;
        if (runCST_.nodeOptional.present()) {
            name =
                (
                    (NodeToken)
                        ((NodeSequence) runCST_.nodeOptional.node).elementAt(
                        0)).tokenImage;
        }

        /***********GET FUNCTION*****************************************/
        QualifiedName invocable = (QualifiedName) runCST_.paraNameCST.accept(this, null);

        /***********GET SCOPE********************************************/
	Scope scope = new GeneralScope(new IntNode(DEFAULT_SCOPE), new TypeScopes());
        if (runCST_.nodeOptional1.present()) {
            scope = (Scope) runCST_.nodeOptional1.node.accept(this, null);
        }
	

        /***********GET EXPECTS******************************************/
        IntNode expects = new IntNode();
        if (runCST_.nodeOptional2.present()) {
            NodeToken number =
                (NodeToken)
                    ((NodeSequence) runCST_.nodeOptional2.node).elementAt(
                    1);
            expects =
                new IntNode(
                    new Location(_fileName, number),
                    Integer.parseInt(number.tokenImage));
        }

        /***********GET LOCATION*****************************************/
        Location location;
        if (runCST_.nodeOptional2.present()) {
            location = new Location(runCST_.nodeToken, expects);
    } else if (runCST_.nodeOptional1.present()) {
            location = new Location(runCST_.nodeToken, scope);
        } else {
            location = new Location(runCST_.nodeToken, invocable);
        }

        return new RunCommand(name, location, scope, expects, invocable);
    }

    /**
     * <PRE>
     * nodeOptional -> [ &lt;ID&gt; &lt;COLON&gt; ]
     * nodeToken -> &lt;CHECK&gt;
     * nodeOptional1 -> [ ParaNameCST() ]
     * nodeOptional2 -> [ ScopeCST() ]
     * nodeOptional3 -> [ &lt;EXPECT&gt; &lt;NUMBER&gt; ]
     * </PRE>
     * @param checkCST_, check Command node of the CST
     * @param argu_ not used
     * @return AST {@link CheckCommand}
     */

    public Object visit(CheckCST checkCST_, Object argu_) {

        /***********GET NAME*****************************************/
        String name = null;
        if (checkCST_.nodeOptional.present()) {
            name =
                (
                    (NodeToken)
                        ((NodeSequence) checkCST_.nodeOptional.node).elementAt(
                        0)).tokenImage;
        }

        /***********GET ASSERTION IDS************************************/
        QualifiedNames assertions = new QualifiedNames();
        if (checkCST_.nodeOptional1.present()) {
            QualifiedName assertName =
                (QualifiedName) checkCST_.nodeOptional1.node.accept(this, null);
            assertions.addQualifiedName(assertName);
        }

        /***********GET SCOPE********************************************/
        Scope scope = new GeneralScope(new IntNode(DEFAULT_SCOPE), new TypeScopes());
        if (checkCST_.nodeOptional2.present()) {
            scope =
                (Scope) ((ScopeCST) checkCST_.nodeOptional2.node).accept(
                    this,
                    null);
        }

        /***********GET EXPECTS******************************************/
        IntNode expects = new IntNode();
        if (checkCST_.nodeOptional3.present()) {
            NodeToken number =
                (NodeToken)
                    ((NodeSequence) checkCST_.nodeOptional3.node).elementAt(
                    1);
            expects =
                new IntNode(
                    new Location(_fileName, number),
                    Integer.parseInt(number.tokenImage));
        }

        /***********GET LOCATION*****************************************/
        Location location;
        if (checkCST_.nodeOptional3.present()) {
            location = new Location(checkCST_.nodeToken, expects);
    } else if (checkCST_.nodeOptional2.present()) {
            location = new Location(checkCST_.nodeToken, scope);
        } else if (checkCST_.nodeOptional1.present()) {
            location = new Location(checkCST_.nodeToken, assertions);
        } else {
            location = new Location(_fileName, checkCST_.nodeToken);
        }

        return new CheckCommand(name, location, scope, expects, assertions);

    }


    /**
     * <PRE>
     * <PRE>
     * nodeChoice -> &lt;FOR&gt; TypeScopeCST() ( &lt;COMMA&gt; TypeScopeCST() )*
     *       | &lt;FOR&gt; &lt;NUMBER&gt; [ &lt;BUT&gt; TypeScopeCST() ( &lt;COMMA&gt; TypeScopeCST() )* ]
     * </PRE>
     * @param scopeCST_, the ScopeCST Node
     * @param argu_ not used
     * @return AST {@link Scope}
     */
    public Object visit(ScopeCST scopeCST_, Object argu_) {
        Scope retScope = null;
        NodeSequence scopeSeq = (NodeSequence) scopeCST_.nodeChoice.choice;

        // switch on which production we have
        switch (scopeCST_.nodeChoice.which) {
            case 0 : // <FOR> TypeScopeCST ( <COMMA> TypeScopeCST )*
                /***********GET TYPESCOPES**********************************/
                TypeScopes typeScopes = getTypeScopes(scopeSeq);
                retScope =
                    new SpecificScope(
                        new Location(
                            (NodeToken) scopeSeq.elementAt(0),
                            typeScopes),
                        typeScopes);
                break;
            case 1 : // <FOR> <NUMBER> [ <BUT> TypeScopeCST ( <COMMA> TypeScopeCST )* ]
                NodeToken numToken = (NodeToken) scopeSeq.elementAt(1);
                IntNode bound =
                    new IntNode(
                        new Location(_fileName, numToken),
                        Integer.parseInt(numToken.tokenImage));
                Location loc =
                    new Location((NodeToken) scopeSeq.elementAt(0), bound);
                TypeScopes specScopes = new TypeScopes();
                // see if any specific scopes have been given
                if (((NodeOptional) scopeSeq.elementAt(2)).present()) {
                    specScopes =
                        getTypeScopes(
                            (NodeSequence)
                                ((NodeOptional) scopeSeq.elementAt(2)).node);
                    loc =
                        new Location(
                            (NodeToken) scopeSeq.elementAt(0),
                            specScopes);
                }
                retScope = new GeneralScope(loc, bound, specScopes);
                break;
        }

        return retScope;
    }

    private TypeScopes getTypeScopes(NodeSequence scopeSeq_) {
        TypeScopes typeScopes = new TypeScopes();
        // scopeSeq_.elementAt(1) has type TypeScopeCST
        TypeScope firstScope =
            (TypeScope) scopeSeq_.elementAt(1).accept(this, null);
        typeScopes.addTypeScope(firstScope);

        TypeScope currentScope = firstScope;

        Enumeration otherTypeScopes =
            ((NodeListOptional) scopeSeq_.elementAt(2)).elements();
        while (otherTypeScopes.hasMoreElements()) {
            // get the TypeScope
            currentScope =
                (TypeScope)
                    ((NodeSequence) otherTypeScopes.nextElement()).elementAt(
                    1).accept(
                    this,
                    null);
            typeScopes.addTypeScope(currentScope);
        }

        typeScopes.setLocation(new Location(firstScope, currentScope));
        return typeScopes;
    }

    /**
     * <PRE>
     * nodeOptional -> [ &lt;EXACTLY&gt; ]
     * nodeToken -> &lt;NUMBER&gt;
     * nodeChoice -> ( SigCST() | &lt;INT&gt; )
     * </PRE>
     * @param typeScopeCST_, the TypeScopeCST node
     * @param argu_, unused
     * @return AST {@link TypeScope}
     */
    public Object visit(TypeScopeCST typeScopeCST_, Object argu_) {
        /********GET BOUND******************/
        int bound = Integer.parseInt(typeScopeCST_.nodeToken.tokenImage);

        /********GET SIGEXPR******************/

        SigExpr sigExpr = null;
        // switch on which production we have
        switch (typeScopeCST_.nodeChoice.which) {
            case 0 : // SigCST
                sigExpr =
                    (SigExpr)
                        ((SigCST) typeScopeCST_.nodeChoice.choice).accept(
                        this,
                        null);
                break;
            case 1 : // <INT>
                NodeToken intToken =
                    (NodeToken) typeScopeCST_.nodeChoice.choice;
                Location location = new Location(_fileName, intToken);
                QualifiedName name =
                    new QualifiedName(
                        location,
                        new Id(location, intToken.tokenImage),
                        new Path());
                sigExpr = new SigExpr(name.getLocation(), name);
                break;
        }

        boolean exact = typeScopeCST_.nodeOptional.present();
        return new TypeScope(
            new Location(typeScopeCST_.nodeToken, sigExpr),
            exact,
            bound,
            sigExpr);
    }


    /****************************************************************
     *                                                              *
     *                                                              *
     *                        PRIVATE METHODS                       *
     *                                                              *
     *                                                              *
     ****************************************************************/

    /**
     * from an enumeration representing comma separated
     * decls, create AST node
     * mutates input Enumeration by calling nextElement() to
     * get the decls
     * @param declSequence_ the decls
     * @return AST {@link Decls}
     */
    private Decls createDecls(Enumeration declSequence_) {
        //get first decl
        Decls decls = new Decls();
        Decl firstDecl =
            (Decl) ((DeclCST) declSequence_.nextElement()).accept(this, null);
        Decl currentDecl = firstDecl;
        NodeListOptional otherDecls =
            (NodeListOptional) declSequence_.nextElement();

        decls.addDecl(firstDecl);

        if (otherDecls.present()) {
            declSequence_ = otherDecls.elements();
            while (declSequence_.hasMoreElements()) {
                currentDecl =
                    (Decl)
                        (
                            (DeclCST)
                                (
                                    (NodeSequence) declSequence_
                                        .nextElement())
                                        .elementAt(
                                1)).accept(
                        this,
                        null);
                decls.addDecl(currentDecl);
            }
        }
        decls.setLocation(new Location(firstDecl, currentDecl));
        return decls;
    }

    /**
     * from an enumeration representing comma separated
     * let decls, create AST node
     * mutates input Enumeration by calling nextElement() to
     * get the let decls
     * @param declSequence_ the let decls
     * @return AST {@link LetDecls}
     */
    private LetDecls createLetDecls(Enumeration declSequence_) {
        //get first decl
        LetDecls decls = new LetDecls();
        LetDecl firstDecl =
            (LetDecl) ((LetDeclCST) declSequence_.nextElement()).accept(
                this,
                null);
        LetDecl currentDecl = firstDecl;
        NodeListOptional otherDecls =
            (NodeListOptional) declSequence_.nextElement();

        decls.addLetDecl(firstDecl);

        if (otherDecls.present()) {
            declSequence_ = otherDecls.elements();
            while (declSequence_.hasMoreElements()) {
                currentDecl =
                    (LetDecl)
                        (
                            (LetDeclCST)
                                (
                                    (NodeSequence) declSequence_
                                        .nextElement())
                                        .elementAt(
                                1)).accept(
                        this,
                        null);
                decls.addLetDecl(currentDecl);
            }
        }
        decls.setLocation(new Location(firstDecl, currentDecl));
        return decls;
    }

    /**
     * from an enumeration representing comma separated
     * exprs, create AST node
     * mutates input Enumeration by calling nextElement() to
     * get the exprs
     * @param exprSequence_ the decls
     * @return AST {@link Exprs}
     */
    private Exprs createExprs(Enumeration exprSequence_) {
        //get first expr
        Exprs exprs = new Exprs();
        Expr firstExpr =
            (Expr) ((ExprCST) exprSequence_.nextElement()).accept(this, null);
        Expr currentExpr = firstExpr;
        NodeListOptional otherExprs =
            (NodeListOptional) exprSequence_.nextElement();

        exprs.addExpr(firstExpr);

        if (otherExprs.present()) {
            exprSequence_ = otherExprs.elements();
            while (exprSequence_.hasMoreElements()) {
                currentExpr =
                    (Expr)
                        (
                            (ExprCST)
                                (
                                    (NodeSequence) exprSequence_
                                        .nextElement())
                                        .elementAt(
                                1)).accept(
                        this,
                        null);
                exprs.addExpr(currentExpr);
            }
        }
        exprs.setLocation(new Location(firstExpr, currentExpr));
        return exprs;
    }

    private void error(String msg, alloy.ast.Node node) {
        alloy.util.Dbg.user(new Msg(msg, node));
    }

    /**
     * creates a binary expansion of a sequence of expressions joined
     * by operators with the same precedence
     * @param leftExpr_ the initial left expression
     * @param nodeEnum_ the enumeration of operators and expressions, modified by calling nextElement()
     * @param op_ the operator to be used for the binary expansions
     * @return the AST {@link Expr}, left-associative binary representation of entire enumeration
     */
    private Expr expandBinaryTree(
        Expr leftExpr_,
        Enumeration nodeEnum_,
        alloy.ast.Node op_) {

        Expr retExpr = leftExpr_;

        while (nodeEnum_.hasMoreElements()) {
            // take the first op and expr, and create a new binary expression
            // using retExpr (done this way because it's left associative)
            NodeSequence curNodeSequence =
                (NodeSequence) nodeEnum_.nextElement();

            /***********GET OP***********************************************/

            alloy.parse.syntaxtree.Node node =
                (alloy.parse.syntaxtree.Node) curNodeSequence.elementAt(0);

            if (node instanceof NodeToken) {
                NodeToken nodeToken = (NodeToken) node;
                Location nodeLocation = new Location(_fileName, nodeToken);
                op_.setLocation(nodeLocation);
            } else {
                alloy.ast.Node opTreeNode = (alloy.ast.Node) node.accept(this, null);
                // take the operator returned by the visit call
                op_ = opTreeNode;
            }

            /***********GET RIGHT EXPR***********************************************/
            Expr rightExpr =
                (Expr)
                    (
                        (
                            alloy
                                .parse
                                .syntaxtree
                                .Node) curNodeSequence
                                .elementAt(
                            1)).accept(
                    this,
                    null);

            /***********GET LOCATION***********************************************/
            Location location = new Location(retExpr, rightExpr);

            retExpr =
                new BinaryExpr(
                    location,
                    retExpr,
                    (BinaryExprOp) op_,
                    rightExpr);
        }

        return retExpr;
    }

    /**
     * creates a binary expansion of a sequence of formulas joined
     * by operators with the same precedence
     * @param leftFormula_ the initial left formula
     * @param nodeEnum_ the enumeration of operators and formulas, modified by calling nextElement()
     * @return the AST {@link Formula}, left-associative binary representation of entire enumeration
     */
    private Formula expandBinaryTree(
        Formula leftFormula_,
        Enumeration nodeEnum_) {

        Formula retFormula = leftFormula_;
        NodeSequence curNodeSequence;

        while (nodeEnum_.hasMoreElements()) {
            // take the first op and formula, and create a new binary formula
            // using retFormula (done this way because it's left associative)
            curNodeSequence = (NodeSequence) nodeEnum_.nextElement();

            /***********GET OP***********************************************/
            alloy.parse.syntaxtree.Node node =
                (alloy.parse.syntaxtree.Node) curNodeSequence.elementAt(0);

            LogicOp op = (LogicOp) node.accept(this, null);

            /***********GET RIGHT FORMULA***********************************************/
            Formula rightFormula =
                (Formula)
                    (
                        (
                            alloy
                                .parse
                                .syntaxtree
                                .Node) curNodeSequence
                                .elementAt(
                            1)).accept(
                    this,
                    null);

            /***********GET LOCATION***********************************************/
            Location location = new Location(retFormula, rightFormula);

            retFormula =
                new BinaryFormula(location, retFormula, op, rightFormula);
        }

        return retFormula;
    }

    private static Specification _getAST(File file_, List parsedModules_, Set importCycles_, 
					 Environment env_, Modules lang_) {
        Reader reader = null;
        try {
            reader = new FileReader(file_);
        } catch (FileNotFoundException fnfe) {
            Dbg.fatal("shouldn't happen");
        }
        return _getAST(file_.getPath(), reader, parsedModules_, importCycles_, env_, lang_);
    }

    /** 
     * get the AST of a CST node that was parsed as a part of the given specification (context)
     * @param node_ cst node to be converted
     * @param context_ specification which is the parsing context for the cst node
     * @return the root of the AST
     **/
    public static alloy.ast.Node getAST(alloy.parse.syntaxtree.Node node_, Specification context_) {
	MakeASTVisitor mav = new MakeASTVisitor(Location.NOT_FROM_FILE, context_);
	return (alloy.ast.Node) node_.accept(mav, null);
    }

    /**
     * get the AST of a specification.
     * @param file_ the file containing the specification.  Assumed to exist.
     * @return the root of the AST
     */
    public static Specification getAST(File file_) {
        return _getAST(file_, new ArrayList(), new HashSet(), new Environment(true),
		       _getLang());
    }

    private static Specification _getAST(String fileName_,
					 Reader reader_,
					 List parsedModules_,
					 Set importCycles_,
					 Environment env_,
					 Modules lang_) {
        return _getAST(fileName_, FileUtil.readIntoString(reader_), 
		       parsedModules_, importCycles_, env_, lang_);
    }

    /**
     * get the AST of a specification
     * @param fileName_ the file name to use in {@link Location}s
     * @param reader_ the reader containing the specification
     * @return the root of the AST
     */
    public static Specification getAST(String fileName_, Reader reader_) {
        return _getAST(fileName_, reader_, new ArrayList(), new HashSet(),
		       new Environment(true), _getLang());
    }

    private static Specification _getAST(String fileName_,
					 String specString_,
					 List parsedModules_,
					 Set importCycles_,
					 Environment env_,
					 Modules lang_) {
        SpecificationCST specCST = null;
        Dbg.addFileToDump(fileName_, specString_);
        //try {
            // first, do prepass
            AlloyPrepass prepass = null;
        	   AlloyPrepass.ParserNames names = null;
            try {
                prepass = new AlloyPrepass(new StringReader(specString_));
                prepass.init();
                prepass.Input();
                names = prepass.getParserNames();
                prepass = null; // free this object; we only need to remember the names
            } catch (ParseException p) {
                String prepassFileName = prepass.getFileName();
                Dbg.user(
                    _getPrepassErrorMessage(
                        p,
                        (prepassFileName == null)
                            ? fileName_
                            : prepassFileName));
                return null;
            } catch (TokenMgrError t) {
                String prepassFileName = prepass.getFileName();
                Dbg.user(
                    _genLexErrorMessage(
                        t,
                        (prepassFileName == null)
                            ? fileName_
                            : prepassFileName));
                return null;
            }
            // then, do regular parse
           // println(debugSwitch, "------------------REGULAR PARSE-------------------");
            try {
                final AlloyParser myParser = new AlloyParser(new StringReader(specString_));
                myParser.init(names);
                specCST = myParser.SpecificationCST();
            } catch (ParseException p) { // exception occurred during parse
                Dbg.user(_getParseErrorMessage(p, fileName_));
                return null;
            } catch (TokenMgrError t) {
                Dbg.user(_genLexErrorMessage(t, fileName_));
                return null;
            }

       // } catch (FileNotFoundException e) {
        //    return null;
       // }


        return (Specification) specCST.accept(new MakeASTVisitor(fileName_, parsedModules_, importCycles_, env_, lang_), names);
    }

    /**
     * get the AST of a specification
     * @param fileName_ the file name to use in {@link Location}s
     * @param specString_ the String containing the specification
     * @return the root of the AST
     */
    public static Specification getAST(String fileName_, String specString_) {
        return _getAST(fileName_, specString_, 
		       new ArrayList(), new HashSet(), new Environment(true),
		       _getLang());
    }

    /**
     * generate an appropriate message for a parse error
     * @param p_ the exception thrown to indicate the error
     */
    private static Msg _getParseErrorMessage(
        ParseException p_,
        String fileName_) {
        return _getMainParseErrorMessage(p_, _stackTraceString(p_), fileName_);
    }

    private static String _stackTraceString(ParseException p_) {
        // for storing stack trace
        ByteArrayOutputStream os = new ByteArrayOutputStream();
        // printing destination
        PrintStream ps = new PrintStream(os);
        p_.printStackTrace(ps);
        String stackTrace = os.toString();
        return stackTrace;
    }
    private static Msg _genLexErrorMessage(TokenMgrError t, String fileName_) {
        String message = t.getMessage();
        String betterMessage = "Lexical error: ";
        betterMessage += message.substring(message.indexOf("Encountered"));
        int lineIndex = message.indexOf("line") + 5;
        int endLineIndex = message.indexOf(",", lineIndex);
        int line = Integer.parseInt(message.substring(lineIndex, endLineIndex));
        int columnIndex = message.indexOf("column", endLineIndex) + 7;
        int endColumnIndex = message.indexOf(".", columnIndex);
        int column =
            Integer.parseInt(message.substring(columnIndex, endColumnIndex));
        return new Msg(
            betterMessage,
            new DummyNode(new Location(fileName_, line, column, line, column)));
    }

    private static alloy.ast.Node _genParseErrorNode(
        ParseException p_,
        String fileName_) {
        Token token = p_.currentToken;
        return new DummyNode(
            new Location(
                fileName_,
                token.next.beginLine,
                token.next.beginColumn,
                token.next.beginLine,
                token.next.beginColumn));
    }

    private static Msg _getMainParseErrorMessage(
        ParseException p_,
        String stackTrace_,
        String fileName_) {
        String basicMessage = p_.getMessage();
        // shorten message to just first line before location
        String shortMessage =
            basicMessage.substring(
                0,
                basicMessage.indexOf("\"", basicMessage.indexOf("\"") + 1) + 1);
        StringBuffer ret = new StringBuffer(shortMessage);
        ret.append(" while trying to parse ");
        ret.append(_getErrorProduction(stackTrace_));
        return new Msg(ret.toString(), _genParseErrorNode(p_, fileName_));
    }

    private static Msg _getPrepassErrorMessage(
        ParseException p_,
        String fileName_) {
        String stackTrace = _stackTraceString(p_);
        String errorProduction = _getErrorProduction(stackTrace);
        String ret = null;
        if (errorProduction.equals("MatchedBraces")) {
            ret = "mismatched braces recognized";
        } else if (errorProduction.equals("MatchedParens")) {
            ret = "mismatched parens recognized";
        } else if (errorProduction.equals("MatchedBrackets")) {
            ret = "mismatched brackets recognized";
        } else if (errorProduction.equals("Input")) {
	    // one of the opened modules does not exist ...
	    Token token = p_.currentToken;
	    Location loc = new Location(fileName_, token.beginLine,
					token.beginColumn, token.endLine,
					token.endColumn); 
	    return new Msg(p_.getMessage(), new DummyNode(loc));
	} else {
            return _getMainParseErrorMessage(p_, stackTrace, fileName_);
        }
        return new Msg(ret, _genParseErrorNode(p_, fileName_));
    }

    private static String _getErrorProduction(String stackTrace_) {
        int curIndex = stackTrace_.indexOf("at alloy.parse");
        // go two lines down
        for (int i = 0; i < 2; i++)
            curIndex = stackTrace_.indexOf('\n', curIndex + 1);
        // forward three dots (alloy.parse.AlloyParser or alloy.parse.AlloyPrepass)
        for (int i = 0; i < 3; i++)
            curIndex = stackTrace_.indexOf('.', curIndex + 1);
        // now, return string up to open paren
        return _getNiceName(
            stackTrace_.substring(
                curIndex + 1,
                stackTrace_.indexOf('(', curIndex)));
    }

    private static String _getNiceName(String production_) {
        if (_productionToName.containsKey(production_)) {
            return (String) _productionToName.get(production_);
        } else {
            return production_;
        }
    }

    /**
     * check if an identifier is shadowing a type variable
     * @param id_ the identifier to check
     * @effects if the identifier is shadowing a type variable prints message to user,
     *    otherwise, does nothing
     */
    private void noShadow(Id id_) {
        // if it's a top level module, no need to check it's type variables
        // otherwise, check and see if anything shadows current module's type variables

        // if there is no alias, then this function is taken care of by
        // alloy.semantic.NoParagraphNameShadowingVisitor
        if(!_environ.isTopLevel()) {
            //if(_environ.hasBinding(id_.nodeString())) {
            if(_environ.hasBinding(new QualifiedName(id_, _curPath))) {

                Dbg.user(new Msg("paragraph " + id_ + " conflicts with type variable", id_));
                return;
            }

            Iterator polyIDs = _polyTypeVarIds.getIdIter();
            while(polyIDs.hasNext()) {
                if (id_.equals(polyIDs.next())) {
                    Dbg.user(new Msg("paragraph " + id_ + " conflicts with type variable", id_));
                }
            }
        }
    }
    
    private void println(boolean flag, Object o) {
    	if(flag) {
    		System.out.println(o);
    	}
    }

    /*
    private Path translateToRealPath(Path path_) {
        Path path = path_;
        // to check if path is an alias,
        // see if the first id in the path's packages corresponds to an alias
        // if it's an alias, swap the alias for the real name
        Id pathAsId = (Id)path_.getPackages().getIdIter().next();
        QualifiedName pathAsName = new QualifiedName(pathAsId, new Path());
        if (_aliasesToModuleNames.containsKey(pathAsName)) {
            // the package name is an alias
            QualifiedName realName = (QualifiedName)_aliasesToModuleNames.get(pathAsName);
            Ids packages = new Ids();
            for (Iterator i = realName.getPath().getPackages().getIdIter(); i.hasNext();) {
                packages.addId((Id)i.next());
            }
            packages.addId(realName.getId());

            path = new Path(path_.getLocation(),packages);

        }

        return path;
    }
    */

}
